proposition: Lemma euclid_fails : ~ (forall (A B C D T : (@Point R 1)), bet' A D T -> bet' B D C -> B <> D -> D <> C -> ~ (bet' A B C \/ bet' B C A \/ bet' C A B) -> exists X Y, bet' A B X /\ bet' A C Y /\ bet' X T Y).
proof: Proof. apply euclid_aux. exists a, b, c, d, t. split ; [exact:bet_adt|]. split ; [exact:bet_bdc|]. split. apply /eqP. by rewrite point_vector_neq /b /d /b'/d' row2_eq -quarter eq_sym mulf_eq0 one_half_neq0. split. apply /eqP. by rewrite point_vector_neq /c/d/c'/d' row2_eq -quarter eq_sym mulf_eq0 one_half_neq0 andbF. have: ~ (bet' a b c \/ bet' b c a \/ bet' c a b)=> [|ncol]. rewrite nbet_abc nbet_cab nbet_bca => H. by repeat (elim H; clear H; intro H). split=> // x. case ((#x) =P b'). move=>-> ? y' bet_acy bet_bty. exfalso. assert (Hacy : Bet (# a) (# c) y') by auto. move: (col_2D' (bet_col _ _ _ Hacy)). assert (Hbty : Bet b' (# t) y') by auto. move: (col_2D' (bet_col _ _ _ Hbty)). rewrite /b' /t' !mxE /= !add0r subrr oppr0 mul0r. rewrite mulf_eq0 oppr_eq0 one_half_neq0 orFb subr_eq0. move=> /eqP <-. by rewrite mulf_eq0 oppr_eq0 one_half_neq0. move => /eqP neq_xb bet_abx y' bet_acy bet_xty. set b1' : 'rV[R]_(2) := (#x) + a' - b'. set k1 := betR a' b1' (#x). have: betS a' b1' (#x). rewrite -bet_betS /b1' ?euclid_fails_aux //; apply /eqP;rewrite a'_eq0. by rewrite addr0 eq_sym subr_eq0. rewrite addr0 -subr_eq0 addrAC subrr sub0r oppr_eq0. by rewrite /b' row2_eq0 one_half_neq0 andbF. move=>/betSP[/eqP ratio_b1_xa k1_gt0 k1_lt1]. rewrite -/k1 in k1_gt0 k1_lt1. set y1' := extension (#a) (#c) k1. suffices: y' = y1'; [move->|]. rewrite /y1' /extension /a /= a'_eq0 addr0 subr0. rewrite -scalemxAl dotC -scalemxAl scalerA mxE. suffices: (c' *m c'^T) 0 0 = 1/(1+1+1+1). move->. apply le_trans with ((1+1) * (1+1) * (1 / (1 + 1 + 1 + 1))). rewrite -quarter !mul1r !mulrA mulrC -!mulrA. rewrite divff ?add11_neq0 //. by rewrite mulr1 mulrC divff ?add11_neq0 ?lexx. apply ler_pmul ; rewrite -?quarter ?mulr_ge0 ?invr_ge0 ?addr_ge0 ?ler01 //. suffices: (1+1) <= k1^-1. move=>?. rewrite ler_pmul ?addr_ge0 ?ler01 //. rewrite /k1 /betR /b1' /ratio. case: pickP => /= [z|/all_v_neq0 H]. rewrite a'_eq0 !mxE /= !subr0 invf_div; case: z => [] [|[| //]] //= p. rewrite (@ord_inj _ (Ordinal p) 0) // => /eqP x00_neq0 . exfalso. apply x00_neq0; apply /eqP. rewrite bet_abx_x00_eq0 //. rewrite (@ord_inj _ (Ordinal p) 1) // =>_. rewrite addr0 ler_pdivl_mulr. rewrite mulrBr mul1r divff ?add11_neq0 //. rewrite -subr_le0 mulrDl !mul1r addrAC -!addrA subrr addr0. rewrite subr_le0 ltW // bet_abx_x01_lt1 //. by rewrite subr_gt0 bet_abx_x01_gt. exfalso; apply H; rewrite subr_eq0 a'_eq0. by apply x_neq0. exact: c'_norm. apply bet_intersect with (#x) (#t) (#a) (#c) (#b). move: ncol; rewrite /bet'=> //. by apply xt_neq. by rewrite eq_sym /a /c /= /a' /c' row2_eq one_half_neq0. by move: bet_abx ; rewrite /bet' bet_sym. by []. by []. set d1':= contraction a' t' k1. set k2:=betR b1' d1' c'. have: extension (#a) d1' k1 == t' ; [|rewrite /t/= => /eqP<-]. by rewrite extension_contraction ?lt0r_neq0. have: extension (#a) b1' k1 == (#x) ; [|clear ratio_b1_xa;move/eqP<-]. rewrite extension_contraction ?lt0r_neq0// /contraction. by rewrite eq_sym -subr_eq. apply euclid'' ; try by []. case: (d1' =P b1') ; [by move ->; rewrite bet_xxa |move=> d1b1_neq]. apply (@bet_b1d1c a' b' b1' c' d' d1' t' (#x)) ;rewrite /=. by []. by rewrite /b1' euclid_fails_aux. by rewrite -/(bet' b d c) bet_bdc. by rewrite -/(bet' a d t) bet_adt. by rewrite /d1' contraction_bet. apply /eqP. by rewrite eq_sym row2_eq -quarter mulf_eq0 one_half_neq0 andFb. apply /eqP. by rewrite row2_eq -quarter mulf_eq0 one_half_neq0 andbF. by move: ncol ;rewrite /Col /bet' /=. by rewrite /b1' a'_eq0 addr0 /cong opprB addrA addcb_eqt. by rewrite /b1' a'_eq0 /cong addr0 subr0 quad_NN. by rewrite a'_eq0 /cong -addcb_eqt -addrA subrr addr0 subr0 eqxx. apply congA_axt_ab1d1. rewrite -bet_betS. by rewrite /b1' euclid_fails_aux. by apply /eqP; rewrite eq_sym /b1' a'_eq0 addr0 subr_eq0. apply /eqP; rewrite /b1' a'_eq0 addr0 -subr_eq0 addrAC subrr. by rewrite add0r oppr_eq0 row2_eq0 one_half_neq0 andbF. rewrite /d1' contraction_betS //. by rewrite a'_eq0 row2_eq0 one_half_neq0. by rewrite /d1' contraction_betR ?eqxx ?row2_eq ?one_half_neq0. by rewrite eq_sym a'_eq0 x_neq0. by rewrite eq_sym xt_neq. by rewrite /b1' a'_eq0 addr0 eq_sym subr_eq0. by apply /eqP. rewrite /b1' /c/= a'_eq0 addr0 -subr_eq0 vector2_neq0. rewrite !mxE /= bet_abx_x00_eq0 //. by rewrite oppr0 !add0r oppr_eq0 one_half_neq0 orTb. by rewrite extension_bet. 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