proposition: Lemma sub_carry : forall xh xl yh yl z, 0 <= z -> [|xh|]*[|yl|] + [|xl|]*[|yh|] = wwB + z -> z < wwB.
proof: Proof. intros xh xl yh yl z Hle Heq. destruct (Z_le_gt_dec wwB z);auto with zarith. generalize (Zmult_lt_b _ _ _ (spec_to_Z xh) (spec_to_Z yl)). generalize (Zmult_lt_b _ _ _ (spec_to_Z xl) (spec_to_Z yh)). rewrite <- wwB_wBwB;intros H1 H2. assert (H3 := wB_pos w_digits). assert (2*wB <= wwB). rewrite wwB_wBwB; rewrite Z.pow_2_r; apply Z.mul_le_mono_nonneg;zarith. lia. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase