proposition: Lemma spec_ww_mod_gt_eq : forall a b, [[a]] > [[b]] -> 0 < [[b]] -> [[ww_mod_gt a b]] = [[snd (ww_div_gt a b)]].
proof: Proof. intros a b Hgt Hpos. change (ww_mod_gt a b) with (match a, b with | W0, _ => W0 | _, W0 => W0 | WW ah al, WW bh bl => if w_eq0 ah then w_0W (w_mod_gt al bl) else match w_compare w_0 bh with | Eq => w_0W (double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl) | Lt => ww_mod_gt_aux ah al bh bl | Gt => W0 end end). change (ww_div_gt a b) with (match a, b with | W0, _ => (W0,W0) | _, W0 => (W0,W0) | WW ah al, WW bh bl => if w_eq0 ah then let (q,r) := w_div_gt al bl in (WW w_0 q, w_0W r) else match w_compare w_0 bh with | Eq => let(q,r):= double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 a bl in (q, w_0W r) | Lt => ww_div_gt_aux ah al bh bl | Gt => (W0,W0) end end). destruct a as [ |ah al];trivial. destruct b as [ |bh bl];trivial. Spec_w_to_Z ah; Spec_w_to_Z al; Spec_w_to_Z bh; Spec_w_to_Z bl. assert (H:=@spec_eq0 ah);destruct (w_eq0 ah). simpl in Hgt;rewrite H in Hgt;trivial. assert ([|bh|] <= 0). apply beta_lex with (d:=[|al|])(b:=[|bl|]) (beta := wB);zarith. assert ([|bh|] = 0) by zarith. rewrite H1 in Hgt;simpl in Hgt. simpl in Hpos;rewrite H1 in Hpos;simpl in Hpos. rewrite spec_w_0W;rewrite spec_w_mod_gt_eq;trivial. destruct (w_div_gt al bl);simpl;rewrite spec_w_0W;trivial. clear H. rewrite spec_compare; case Z.compare_spec; intros H2. rewrite (@spec_double_modn1_aux w w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_w_0 spec_compare 1 (WW ah al) bl). destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl);simpl;trivial. rewrite spec_ww_mod_gt_aux_eq;trivial;symmetry;trivial. trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub