proposition: Lemma segment_construction_aux a b c d : a!=b -> c!=d -> exists E' : Vector, bet (#a) (#b) E' /\ cong_v (#b) E' (#c) (#d).
proof: Proof. move=> ab_neq cd_neq. set K := omd b b/dist c d. set pab := ((#a)*m(#b)^T) 0 0. set c1 := (norm(#b)^+2 - pab)^+2 + K * norm(#a - #b)^+2. set c2 := 2%:R * ( K * (pab - norm(#a)^+2) + omd a b * (pab - norm(#b)^+2) ). set c3 := (omd a b)^+2 - K* omd a a. set delta := c2^+2 - 4%:R * c1 * c3. have: 0 < delta. suffices : 0 < delta / 4%:R / (omd a a * omd b b) ^+ 2. rewrite !pmulr_lgt0 ?invr_gt0 ?ltr0n //. by rewrite expr2 ?mulr_gt0 ?omd_gt0. have: delta/4%:R/(omd a a* omd b b)^+2 == ((omd a b/omd a a)^+2 - omd b b/ omd a a) * ((1/dist c d)^+2 - 1/dist c d). rewrite /delta [X in X/_==_]mulrBl [4%:R * c1 * c3 /4%:R]mulrC. rewrite mulrA mulrA [_^-1*_]mulrC divff ?lt0r_neq0 ?ltr0n //. rewrite !mul1r [X in X==_]mulrBl. have: 4%:R == (2%:R)^+2 :> R by rewrite expr2 /GRing.natmul /= mulrDl !mul1r !addrA. move=> /eqP ->. rewrite -exprVn -exprMn -exprVn -exprMn. rewrite [X in _ - c1 *_ *X]expr2 mulrA. rewrite [c1 * c3 /_]mulrAC -[c1/_*_/_]mulrA. rewrite segment_construction_aux1. rewrite segment_construction_aux2. rewrite segment_construction_aux3. rewrite !mul1r. rewrite segment_construction_aux4. rewrite segment_construction_aux5. rewrite !opprD !opprK !addrA. rewrite -[_+ dist a b ^- 2 - dist a b ^- 2]addrA subrr addr0. rewrite -[_ -dist c d ^- 2 * (1 - 2%:R * omd a b / omd a a)]addrA. rewrite subrr addr0. rewrite -[ _ + 2%:R / dist a b * omd a b / omd a a ]addrA. rewrite [_ + 2%:R / dist a b * omd a b / omd a a ]addrC. rewrite subrr addr0. rewrite -[ _ - 2%:R / dist c d * (omd a b / omd a a)]addrA subrr addr0. rewrite -[_+2%:R / dist c d / dist a b * (1 - omd a b / omd a a)]addrA. rewrite [_+2%:R / dist c d / dist a b * (1 - omd a b / omd a a)]addrC. rewrite subrr addr0. rewrite segment_construction_aux6. rewrite -[_ - (omd a b/ omd a a)^+2]addrA subrr addr0. rewrite exprMn /GRing.natmul /=. rewrite -[_ + (dist c d)^-1 * (omd a b / omd a a) ^+ 2]addrA. rewrite [_ + (dist c d)^-1 * (omd a b / omd a a) ^+ 2]addrC. rewrite subrr addr0 -mulrBl addrAC -addrA -mulrBl exprVn. rewrite -[(dist c d)^-1 - dist c d ^- 2]opprB. by rewrite mulNr -mulrBr mulrC eqxx. move=> /eqP ->. rewrite mulr_gt0 // exprMn !expr2 mulrA -mulrBl. rewrite -expr2 mulr_gt0 ?invr_gt0 ?omd_gt0 //. rewrite -[_/omd a a]mulr1 -(@divff R (omd b b)) ?omd_eq0 //. rewrite mulrA mulrAC -[X in _ -X]mul1r -mulrBl. rewrite mulr_gt0 ?omd_gt0 // -mulrA -invfM. rewrite subr_gt0 -invf_lt1; last by rewrite expr2 invfM ?mulr_gt0 ?invr_gt0 ?omd_gt0. by rewrite invf_div -/(dist_v _ _) -/(dist _ _) dist_lt1. rewrite !mul1r mulr_gt0 ?invr_gt0 ?dist_gt0 //. by rewrite subr_gt0 invf_gt1 ?dist_gt0 ?dist_lt1. move => delta_gt0. set r1 := (- c2 - Num.sqrt delta) / 2%:R / c1. set r2 := (- c2 + Num.sqrt delta) / 2%:R / c1. set E1' := extension (#a) (#b) r1^-1. set E2' := extension (#a) (#b) r2^-1. have: cong_v (#b) E1' (#c) (#d) /\ cong_v (#b) E2' (#c) (#d). move: (@roots_poly2 c1 c2 c3) => H. destruct H as [Hr1 Hr2]. rewrite lt0r_neq0 // /c1 addrC addr_ge_gt0 ?sqr_ge0//. by rewrite /K ?mulr_gt0 ?invr_gt0 ?dist_gt0 ?omd_gt0 ?norm_point_subr_gt0 //; rewrite eq_sym ab_neq. by rewrite -/delta ltW. by rewrite (@poly_cong a b c d r1) ?(@poly_cong a b c d r2). have: E1' != E2'. rewrite /E1' /E2' /extension -subr_eq0. rewrite addrAC opprD !addrA -addrA [-#a +#a]addrC subrr addr0. rewrite -scalerBl scaler_eq0 Bool.negb_orb !subr_eq0. rewrite [#b == #a]eq_sym ab_neq andbT. rewrite /r1/r2 !invf_div. apply /negPf. rewrite -subr_eq0 -!mulrBl. apply /eqP /eqP. rewrite ?mulf_neq0 ?invr_neq0 ?[2%:R!=0]lt0r_neq0 ?ltr0n //. case: (c2 =P 0). move->. rewrite oppr0 !add0r subr_eq0 eq_sym -subr_eq0. by rewrite opprK lt0r_neq0 ?addr_gt0 ?sqrtr_gt0. move=> /eqP c2_neq0. rewrite subr_eq0. move: (lt_total c2_neq0). move=>/orP[c2_lt0|c2_gt0]. rewrite ?invr_eq0 ?lt0r_neq0 ?addr_gt0 ?oppr_gt0 ?sqrtr_gt0 //. rewrite -subr_eq0 opprD opprK addrCA !addrA subrr add0r -opprD. by rewrite oppr_eq0 lt0r_neq0 ?addr_gt0 ?sqrtr_gt0. rewrite eq_sym -opprD ?invr_eq0 ?oppr_eq0 ?lt0r_neq0 ?addr_gt0 ?oppr_gt0 ?sqrtr_gt0 //. rewrite -subr_eq0 opprK addrCA !addrA subrr add0r. by rewrite lt0r_neq0 ?addr_gt0 ?sqrtr_gt0. rewrite lt0r_neq0 // /c1 addrC addr_ge_gt0 ?sqr_ge0//. by rewrite /K ?mulr_gt0 ?invr_gt0 ?dist_gt0 ?omd_gt0 ?norm_point_subr_gt0 //; rewrite eq_sym ab_neq. move => /eqP E1'E2'_neq [cong1 cong2]. suffices: bet (#a) (#b) E1' \/ bet (#a) (#b) E2'. move => [? | ?] ; [by exists E1' | by exists E2']. apply /orP. have: bet (# a) (# b) E1' \/ bet (# b) E1' (# a) \/ bet E1' (# a) (# b) by apply (@extension_col R n.+1 (#a) (#b) E1' r1^-1); rewrite /E1'. move=>[-> //|one_side_E1']. have: bet (# a) (# b) E2' \/ bet (# b) E2' (# a) \/ bet E2' (# a) (# b) by apply (@extension_col R n.+1 (#a) (#b) E2' r2^-1); rewrite /E2'. move=>[-> |one_side_E2']. by rewrite orbT. exfalso. apply E1'E2'_neq; apply /eqP. set eps := ((1-norm(#b))/2%:R/norm(#b-#a)). have: 0 < eps by rewrite /eps ?mulr_gt0 ?subr_gt0 ?invr_gt0 ?norm_point_lt1 ?ltr0n ?norm_point_subr_gt0. move=> eps_gt0. set f' := extension (#a) (#b) ((eps+1)^-1). have: (f' *m (f')^T)0 0 <1. suffices: norm(f') < 1. move=> ?. by rewrite -norm_sqr expr2 mulr_ilt1 ?norm_ge0. rewrite /f'/extension invrK scalerDl scale1r addrA. rewrite -addrA [-#a+#a]addrC subrr addr0. apply le_lt_trans with (norm(eps*:(#b-#a)) + norm(#b)). exact: triangle_ineq. rewrite /norm -scalemxAl dotC -scalemxAl scalerA mxE. rewrite sqrtrM; last by rewrite mulr_ge0 ?ltW. rewrite sqrtr_sqr ger0_norm ?ltW // /eps -/(norm _). rewrite -mulrA [(norm (_))^-1 * norm (_)]mulrC divff; last by rewrite lt0r_neq0 ?norm_point_subr_gt0. rewrite mulr1 -/(norm _) mulrBl -addrA [X in _ + (X)]addrC. rewrite -{1}[norm(#b)]mulr1 -mulrBr one_sub_half -mulrDl divf_lt1 ?ltr0n //. rewrite /GRing.natmul /= -subr_lt0 opprD addrAC addrA subrr. by rewrite sub0r addrC subr_lt0 norm_point_lt1. move=> f'_in_disk. set f := (exist (fun p => (p *m p^T) 0 0 < 1) f' f'_in_disk). have: bet' f b a by rewrite /bet' bet_sym extension_bet ?invr_gt0 ?invf_lt1 ?addr_gt0 // -subr_gt0 -addrA subrr addr0. move=> bet_fba. set E1 := (exist (fun p => (p *m p^T) 0 0 < 1) E1' (E_in_disk_aux cong1)). set E2 := (exist (fun p => (p *m p^T) 0 0 < 1) E2' (E_in_disk_aux cong2)). suffices: (E1 == E2) by rewrite point_vector_eq /=. apply one_side_cong'_eq with f b. move: one_side_E1' => [|bet_E1'ab]. by apply POF_to_Tarski.bet_inner_transitivity. rewrite bet_sym in bet_E1'ab. apply bet_outer_transitivity' with (#a)=> //. by rewrite eq_sym -point_vector_neq. move: one_side_E2'=> [|bet_E2'ab]. by apply POF_to_Tarski.bet_inner_transitivity. rewrite bet_sym in bet_E2'ab. apply bet_outer_transitivity' with (#a)=>//. by rewrite eq_sym -point_vector_neq. exact: (@cong_inner_transitivity_vector (# b) E1' (# b) E2' (#c) (#d)). rewrite point_vector_neq. rewrite /=/f'/extension invrK scalerDl scale1r. rewrite !addrA -addrA [-#a+#a]addrC subrr addr0 -subr_eq0. rewrite -addrA subrr addr0 scaler_eq0 subr_eq0 [#b==#a]eq_sym. by rewrite Bool.negb_orb lt0r_neq0. 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