proposition: Lemma sum_mul_carry : forall xh xl yh yl wc cc beta, 1 < beta -> 0 <= wc < beta -> 0 <= xh < beta -> 0 <= xl < beta -> 0 <= yh < beta -> 0 <= yl < beta -> 0 <= cc < beta^2 -> wc*beta^2 + cc = xh*yl + xl*yh -> 0 <= wc <= 1.
proof: Proof. nia. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia