proposition: Theorem lt_mult_inv : forall a b c : nat, a * b < a * c -> b < c.
proof: Proof. intros a; case a. intros b c H1; inversion H1. intros a1 b c H; case (Nat.le_gt_cases c b); auto; intros H1. absurd (S a1 * c <= S a1 * b); auto with arith. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)