proposition: Lemma div_gt_fold : div_gt = div_gt_folded.
proof: Proof. lazy beta iota delta [iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t]. reflexivity. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen