proposition: Theorem mult_add_ineq2: forall x y c cross beta, 0 <= x < beta -> 0 <= y < beta -> 0 <= c*beta + cross <= 2*beta - 2 -> 0 <= x * y + (c*beta + cross) < beta^2.
proof: Proof. nia. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia