proposition: Lemma congA_axt_ab1d1 (a b1 d1 t x : @Vector R 1) : betS a b1 x -> betS a d1 t -> betR a b1 x == betR a d1 t -> a != x -> t != x -> a != b1 -> d1 != b1 -> CongA a x t a b1 d1.
proof: Proof. rewrite /CongA. move=> /betSP[bet_eq_ab1x k_gt0 k_lt1] /betSP[bet_eq_ad1t _ _] /eqP betR_eq /eqP ax_neq /eqP tx_neq /eqP ab1_neq /eqP d1b1_neq. repeat (split; first by []). clear ax_neq tx_neq ab1_neq d1b1_neq. set k := betR a b1 x. rewrite -/k in k_gt0. rewrite -/k in k_lt1. set k2 := (k / (k+1)). set k3 := (1 / (k+1)). have: (k2 > 0) by rewrite /k2 mulr_gt0 ?invr_gt0 ?addr_gt0 ?ltr01. have: (k2 < 1). by rewrite /k2 divf_lt1 ?cpr_add ?addr_gt0 ?ltr01. have: (k3 > 0) by rewrite /k3 mulr_gt0 ?invr_gt0 ?addr_gt0 ?ltr01. have: (k3 < 1) by rewrite /k2 divf_lt1 ?cpr_add ?addr_gt0 ?ltr01. have: k != 0 by rewrite lt0r_neq0. move=>k_neq0. have: d1 - b1 == k *: (t - x). have: d1 - b1 = (d1 - a) + (a - b1). by rewrite addrA [X in _ = X]addrC !addrA [X in _ = X]addrAC -!addrA subrr addr0 addrC. have: t - x = (t - a) - ( x - a) by rewrite opprB addrA [X in _ = X]addrC !addrA [X in _ = X]addrAC -!addrA subrr addr0 addrC. move=> -> ->. rewrite scalerDr -[a - b1]opprB scalerN. rewrite bet_eq_ad1t bet_eq_ab1x. by rewrite /k betR_eq. move=> /eqP keq_d1b1_tx. exists (extension x a k3). exists (extension x t k3). exists (extension b1 a k2). exists (extension b1 d1 k2). rewrite /= !extension_bet //. repeat (split; first try (by [])). rewrite /extension /k3 invf_div mulrDl divff ?oner_neq0 //. rewrite divr1 scalerBr !scalerDl !scale1r opprD -!addrA. rewrite [- x + x]addrC subrr addr0 !addrA addrAC. rewrite /cong -!addrA subrr addr0 -!scalerBr. by rewrite quad_NN quad_kNN bet_eq_ab1x. rewrite /extension /k3 invf_div mulrDl divff ?oner_neq0 //. rewrite divr1 scalerBr !scalerDl !scale1r opprD -!addrA. rewrite [- x + x]addrC subrr addr0 !addrA addrAC. rewrite /cong -!addrA subrr addr0 -!scalerBr. by rewrite keq_d1b1_tx eqxx. rewrite /extension /k2 invf_div mulrDl divff ?k_neq0 //. rewrite mul1r scalerBr !scalerDl !scale1r opprD -!addrA. rewrite [- b1 + (- (k^-1 *: b1) + b1)]addrC -!addrA subrr addr0. rewrite addrC /cong -!addrA subrr addr0 -!scalerBr. rewrite quad_kNN quad_NN bet_eq_ab1x. by rewrite scalerA mulrC divff ?k_neq0 ?scale1r. rewrite /extension /k2 invf_div mulrDl divff ?k_neq0 //. rewrite mul1r scalerBr !scalerDl !scale1r opprD -!addrA. rewrite [- b1 + (- (k^-1 *: b1) + b1)]addrC -!addrA subrr addr0. rewrite addrC /cong -!addrA subrr addr0 -!scalerBr. by rewrite keq_d1b1_tx scalerA mulrC divff ?k_neq0 ?scale1r. rewrite /extension /k3 invf_div mulrDl divff ?oner_neq0 //. rewrite divr1 scalerBr !scalerDl !scale1r opprD -!addrA. rewrite [- x + x]addrC subrr !addr0. rewrite /extension /k2 invf_div mulrDl divff ?k_neq0 //. rewrite mul1r !scalerBr !scalerDl !scale1r opprD -!addrA. rewrite [- b1 + (- (k^-1 *: b1) + b1)]addrC -!addrA subrr addr0. rewrite !addrA addrC [X in cong _ X _ _]addrAC. rewrite [X in cong _ _ X _]addrC. rewrite /cong !opprD !opprK !addrA. rewrite addrC !addrA addrC !addrA addrAC -!addrA subrr addr0. rewrite !addrA addrAC addrC !addrA -scalerBr addrAC. rewrite eq_sym. rewrite addrC !addrA addrC !addrA. rewrite addrAC -!addrA subrr addr0. rewrite !addrA addrAC addrC !addrA addrAC -!addrA -scalerBr. rewrite !addrA bet_eq_ad1t -betR_eq -/k. by rewrite scalerA -!addrA mulrC divff ?k_neq0 ?scale1r. 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