fact: Definition gcd (a b : t) : t := match compare a b with | Eq => a | Lt => gcd_gt b a | Gt => gcd_gt a b end.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen