proposition: Lemma divf_le1 (a b: R): 0 < b -> a / b <= 1 = (a <= b).
proof: Proof. move=> b_g0. suffices: (a/b <= b/b) = (a <= b). by move<- ; rewrite divff ?lt0r_neq0. by rewrite -subr_le0 -mulrBl pmulr_lle0 ?invr_gt0 ?subr_le0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence