fact: Definition div_eucl (x y : t) : t * t := if eqb y zero then (zero, ltac:(match eval hnf in (1 mod 0) with | 0 => exact zero | _ => exact x end)) else match compare x y with | Eq => (one, zero) | Lt => (zero, x) | Gt => div_gt x y end.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen