proposition: Lemma ratio_cp'_aux_1 (a b c : R) : b - a != 0 -> 1 < (b - a) / (c - a) -> 0 < (c - b) / (a - b) < 1.
proof: Proof. rewrite subr_eq0 eq_sym -{1}[b]add0r -subr_eq0 add0r=> ? ?. have: (0 < ((b - a) / (c - a)))=> [|H]. by apply le_lt_trans with 1; rewrite ?ler01. rewrite andbC -subr_lt0 andbC -(ltr_addr (-1)) -[1]divr1. rewrite {1}divr1 -mulNr addf_div ?oner_neq0 // !mulr1 mulNr mul1r opprB addrBDB. by rewrite -[a - b]opprB invrN mulrN oppr_lt0 -[X in _ < X]mulN1r ltr_nmulr; rewrite ?oppr_lt0 ?ltr01 // -invf_div invr_gt0 H andbT invf_cp1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq order) mathcomp(fintype bigop) mathcomp(ssralg ssrnum matrix) mathcomp(zmodp) GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Meta_theory.Counter_models.coplanarity GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Tarski_dev.Ch12_parallel_inter_dec