proposition: Theorem Zlt_square_mult_inv: forall a b, 0 <= a -> 0 <= b -> a * a < b * b -> a < b.
proof: Proof. intros a b H1 H2 H3; case (Zle_or_lt b a); auto; intros H4; apply Zmult_lt_reg_r with a; contradict H3; apply Zle_not_lt; apply Zle_square_mult; auto. Qed.
imports: ArithRing ZArith Zpow_facts Znumtheory Tactic