fact: Definition mul : t -> t -> t := Eval lazy beta iota delta [iter_sym dom_op dom_t reduce succ_t extend zeron wn_mul DoubleMul.w_mul_add mk_t_w'] in mul_folded.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen