proposition: Lemma spec_ww_mod_gt_aux_eq : forall ah al bh bl, ww_mod_gt_aux ah al bh bl = snd (ww_div_gt_aux ah al bh bl).
proof: Proof. intros ah al bh bl. unfold ww_mod_gt_aux, ww_div_gt_aux. case w_compare; auto. case w_div32; auto. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub