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