proposition: Lemma mult_lt_lt : forall p p' k, p * k < p' * k -> p < p'.
proof: Proof. intros p p' k Hin; case (le_lt_dec p' p); [| trivial]. - intros p_in; rewrite lt_nge in Hin; contradict Hin. now apply Nat.mul_le_mono. Qed.
imports: Coq(Arith Lia )