proposition: Lemma betS_ratio a b c (r := betR a b c) : betS a b c -> (c - b = ((1 - r) / r) *: (b - a)).
proof: Proof. move=> b1. have: betS c b a by rewrite betS_sym. rewrite betS_neq13; move: b1. move=> /betSP[E1 ? ?] /andP[/betSP[E2 ? ?]?]. apply /eqP; rewrite -opprB E1 E2. rewrite eq_div_scale /r ?lt0r_neq0 // sub_1_ratio ?subr_eq0 // opprB addrBDB. by rewrite /betR -scalerN opprB !scalerA mulrC -opprB ratioNr -ratiorN opprB. 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