proposition: Lemma bet_cong_ratio_eq a b c a' b' c' (r := betR a b c) (r' := betR a' b' c') : betS a b c -> betS a' b' c' -> cong b a b' a' -> cong b c b' c' -> (1 - r) / r = (1 - r') / r'.
proof: Proof. rewrite /cong betS_neq12=> /andP[b1 NE] b2 /eqP c1 /eqP c2. suff: ((((1 - r) / r)^+2 - ((1 - r') / r')^+2)*:((a - b) *m (a - b)^T) == 0). rewrite scaler_eq0 ?quad_eq0 ?subr_eq0=> /orP[|/eqP E]; rewrite ?eqf_sqr; last by rewrite E in NE; move/eqP: NE=> //. move=> /orP[/eqP ->//|]. rewrite eq_sym -sub0r subr_eq=>/eqP E. have: (0 < (1 - r) / r + (1 - r') / r'); first by rewrite addr_gt0 ?betS_gt0 //. by rewrite lt0r -E eqxx andFb //. rewrite scalerBl {2}c1 subr_eq0 !expr2 -scalerA scalemxAl dotC. rewrite scalemxAl eq_sym -scalerA scalemxAl dotC scalemxAl. rewrite -[a - b]opprB -[a'-b']opprB !scalerN -(betS_ratio b2) -(betS_ratio b1). by rewrite !mulNmx dotC [X in _ == -X]dotC !mulNmx c2. 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