refactor(library/logic/connectives): mark theorems used to prove 'decidable' theorems as transparent

if we don't this, then 'if-then-else' expressions depending on theorems
such as 'and_decidable', 'or_decidable' will not compute inside the kernel
refactor(library/data/nat): prove auxiliary theorems about < and sub asap for the definitional package
feat(library/logic/if): add dependent if-then-else: dite
test(tests/lean/run/div_wf): cleanup div based on well founded recursion
fix(library/logic/wf): typo
feat(library/logic/default): add wf_k
feat(library/data/nat): add more basic theorems for definitional package
refactor(library/data/nat/div): use well-founded library for defining div, mod and gcd
feat(library/data/nat/div): remove some 'sorry's
feat(library/data/nat/decl): add 'measure'
refactor(library/data/nat/div): simplify 'gcd' definition
fix(library/data/nat/div): notation should be local
fix(tests/lean): adjust tests since module 'logic' depends on nat

We need that because of the definitional package
feat(hott/types/sigma): port large part of the sigma library from the hott library

most importantly, prove the characterization of paths in sigma types
feat(hott/path): add notation for higher and dependent transports
fix(hott/trunc): comment out sorry
refactor(data.prod): move theorems about products from data.quotient.util to data.prod.thms
refactor(data/sigma): move notation from sigma.thms to sigma.decl
feat(hott/types): port more of the sigma library from Coq

prove theorems about interaction of sigma types and n-types, including the fact that sigmas preserve n-types
fix(hott/path): make recursion-like definitions reducible