proposition: Lemma Rlt_div_r : forall a b c, c > 0 -> (a * c < b <-> a < b / c).
proof: Proof. split ; intros. replace a with ((a * c) / c) by (field ; apply Rgt_not_eq, H). apply Rmult_lt_compat_r. apply Rinv_0_lt_compat, H. apply H0. replace b with ((b / c) * c) by (field ; apply Rgt_not_eq, H). apply Rmult_lt_compat_r. apply H. apply H0. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)