proposition: Lemma spec_ww_square_c : forall x, [||ww_square_c x||] = [[x]]*[[x]].
proof: Proof. destruct x as [ |xh xl];simpl;trivial. case_eq match ww_add_c (w_mul_c xh xl) (w_mul_c xh xl) with | C0 cc => (w_0, cc) | C1 cc => (w_1, cc) end;intros wc cc Heq. apply (spec_mul_aux xh xl xh xl wc cc);trivial. generalize Heq (spec_ww_add_c (w_mul_c xh xl) (w_mul_c xh xl));clear Heq. rewrite spec_w_mul_c;destruct (ww_add_c (w_mul_c xh xl) (w_mul_c xh xl)); unfold interp_carry;try rewrite Z.mul_1_l;intros Heq Heq';inversion Heq; rewrite (Z.mul_comm [|xl|]);subst. rewrite spec_w_0;rewrite Z.mul_0_l;rewrite Z.add_0_l;trivial. rewrite spec_w_1;rewrite Z.mul_1_l;rewrite <- wwB_wBwB;trivial. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase