proposition: Lemma mult_inj_l : forall a b c : nat, a * c < b * c -> a < b.
proof: Proof. intros. case (le_or_lt b a); [ intro | auto with arith ]. absurd (b * c <= a * c); auto with arith. Qed.
imports: Arith Constants Le_lt_compl