Commit 2022-12-12 05:12 8ecca6f9

feat port: Algebra.EuclideanDomain.Basic (#919) 655994e298904d7e5bbd1e18c95defd7b543eb94 I also added some #align in Logic.Basic and added the theorem by_cases which is aligned to classical.by_cases in Lean3 There is one very ugly proof of xgcdAux_P because I wasn't sure how best to prove a statement like ∀ {x : α}, p x when I don't want to introduce the variable x