proposition: Lemma ratio_cp' (a b c : R) : b - a != 0 -> c - a != 0 -> b - c != 0 -> [|| 0 < (b - a) / (c - a) < 1, 0 < (c - b) / (a - b) < 1 | 0 < (a - c) / (b - c) < 1].
proof: Proof. move=> H1 H2 H; have: ((b - a) / (c - a) != 1)=> [|H4]. rewrite -[X in _ != X]add0r -subr_eq -[1]divr1 -mulNr addf_div ?oner_neq0 //. by rewrite !mulr1 mulNr mul1r opprB addrBDB mulf_neq0 // invr_neq0. have: ((c - b) / (a - b) != 1)=> [|H5]. rewrite -[X in _ != X]add0r -subr_eq -[1]divr1 -mulNr addf_div ?oner_neq0 //; rewrite ?mulr1 ?mulNr ?mul1r ?opprB ?addrBDB ?mulf_neq0 // ?invr_neq0 //; by rewrite subr_eq add0r eq_sym -[X in _ != X]add0r -subr_eq. move: (lt_total H1) (lt_total H2)=> /orP[L1|G1] /orP[L2|G2]. have: (0 < (b - a) / (c - a)); first by rewrite nmulr_lgt0 // invr_lt0. move: (lt_total H4)=> /orP[->->//=|G1 ?]; move: (lt_gtF G1)=> ->. by rewrite andbF /= ratio_cp'_aux_1. have: ((b - a) / (c - a) < 0); first by rewrite nmulr_rlt0 // invr_gt0. move=> L2; move: (lt_gtF L2)=> -> /=; apply ratio_cp'_aux_2 in L2=> //; last by rewrite subr_eq add0r eq_sym -[X in _ != X]add0r -subr_eq. move: (lt_total H5) L2=> /orP[->->//=|G1 ?]; move: (lt_gtF G1)=> ->. by rewrite andbF /= ratio_cp'_aux_1 //; rewrite subr_eq add0r eq_sym -[X in _ != X]add0r -subr_eq. have: ((b - a) / (c - a) < 0); first by rewrite pmulr_rlt0 // invr_lt0. move=> L1; move: (lt_gtF L1)=> -> /=; apply ratio_cp'_aux_2 in L1=> //; last by rewrite subr_eq add0r eq_sym -[X in _ != X]add0r -subr_eq. move: (lt_total H5) L1=> /orP[->->//=|G2 ?]; move: (lt_gtF G2)=> ->. by rewrite andbF /= ratio_cp'_aux_1 //; rewrite subr_eq add0r eq_sym -[X in _ != X]add0r -subr_eq. have: (0 < (b - a) / (c - a)); first by rewrite pmulr_rgt0 // invr_gt0. move: (lt_total H4)=> /orP[->->//=|G3 ?]; move: (lt_gtF G3)=> ->. by rewrite andbF /= ratio_cp'_aux_1. 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