proposition: Lemma spec_double_mul_c : forall cross:w->w->w->w->zn2z w -> zn2z w -> w*zn2z w, (forall xh xl yh yl hh ll, [[hh]] = [|xh|]*[|yh|] -> [[ll]] = [|xl|]*[|yl|] -> let (wc,cc) := cross xh xl yh yl hh ll in [|wc|]*wwB + [[cc]] = [|xh|]*[|yl|] + [|xl|]*[|yh|]) -> forall x y, [||double_mul_c cross x y||] = [[x]] * [[y]].
proof: Proof. intros cross Hcross x y;destruct x as [ |xh xl];simpl;trivial. destruct y as [ |yh yl];simpl. rewrite Z.mul_0_r;trivial. assert (H1:= spec_w_mul_c xh yh);assert (H2:= spec_w_mul_c xl yl). generalize (Hcross _ _ _ _ _ _ H1 H2). destruct (cross xh xl yh yl (w_mul_c xh yh) (w_mul_c xl yl)) as (wc,cc). intros;apply spec_mul_aux;trivial. rewrite <- wwB_wBwB;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase