proposition: Lemma five_segment : five_segmentP Point bet' cong'.
proof: Proof. move=> a a' b b' c c' d d'. move=> cong1 cong2 cong3 cong4 bet1 bet2 /eqP /negPf ab_neq. move: bet1 cong1 cong2 cong3 cong4. rewrite point_vector_eq in ab_neq. rewrite /bet /cong' => /orP[/betEP[[/eqP]|/eqP|->]|]; rewrite ?ab_neq //. rewrite cong_v_aabc=> _ /eqP -> //. move=> betS_abc. move:bet2. rewrite /bet => /orP[/betEP[[-> _]|->|->]|]; rewrite ?cong_v_bcaa ?ab_neq //. move=> _ /eqP -> //. move=> betS_a'b'c'. rewrite -!/(cong' _ _ _ _)-!dist_cong'. move=> /eqP dist_ab /eqP dist_bc /eqP dist_ad /eqP dist_bd. have: (#c) = extension (#a) (#b) (betR (#a) (#b) (#c)) by apply betS_extension. have: (#c') = extension (#a') (#b') (betR (#a') (#b') (#c')) by apply betS_extension. rewrite /extension. set l := (betR (#a) (#b) (#c))^-1. set l' := (betR (#a') (#b') (#c'))^-1. rewrite scalerBr addrAC -[X in _ + X -_]scale1r -addrA. rewrite -scalerBl addrC. move => c'_eq. rewrite scalerBr addrAC -[X in _ + X -_]scale1r -addrA. rewrite -scalerBl addrC. move => c_eq. rewrite (five_segment_aux a c d) (five_segment_aux a' c' d'). set mu := l * Num.sqrt(omd b b/ omd a a). set mu' := l' * Num.sqrt(omd b' b'/ omd a' a'). have: mu != 0 by rewrite /mu /l mulf_neq0 ?invr_neq0 ?betR_neq0 ?lt0r_neq0 ?sqrtr_gt0 ?mulr_gt0 ?invr_gt0 ?omd_gt0. have: mu' != 0 by rewrite /mu /l mulf_neq0 ?invr_neq0 ?betR_neq0 ?lt0r_neq0 ?sqrtr_gt0 ?mulr_gt0 ?invr_gt0 ?omd_gt0. move=> mu'_neq0 mu_neq0. rewrite (@five_segment_aux2 a b c l mu) ?c_eq //. rewrite (@five_segment_aux2 a' b' c' l' mu') ?c'_eq //. rewrite (@five_segment_aux3 a b c d l mu) ?c_eq //. rewrite (@five_segment_aux3 a' b' c' d' l' mu') ?c'_eq //. have : (1-l)/mu == (1-l')/mu'. suffices: (1-l)/l * (omd a a/ omd a b) == (1-l')/l' * (omd a' a'/ omd a' b'). rewrite (@five_segment_aux4 a b). rewrite (@five_segment_aux4 a' b'). rewrite [omd a a * dist a b / omd b b]mulrAC. rewrite [omd a' a' * dist a' b' / omd b' b']mulrAC. rewrite sqrtrM ?mulr_ge0 ?invr_ge0 ?omd_ge0 //. rewrite [Num.sqrt (omd a' a' / omd b' b' * dist a' b')]sqrtrM ?mulr_ge0 ?invr_ge0 ?omd_ge0 //. rewrite -subr_eq0 dist_ab mulrA mulrA -mulrBl mulf_eq0. rewrite sqrtr_eq0 /dist/dist_v -!/(omd _ _) -{2}(mul1r (omd a' a')). rewrite expr2 invfM mulrA. rewrite !pmulr_lle0 ?invr_gt0 ?omd_gt0 //. rewrite ler10 orbF subr_eq0 /mu/mu' !invfM. by rewrite !sqrt_invf !invf_div !mulrA. suffices: (omd a c/l/omd a b)^+2 == (omd a' c'/l'/omd a' b')^+2. rewrite eqf_sqr =>/orP[|]. rewrite [omd a c]omd_reflexivity [omd c a]/omd/omd_v c_eq. rewrite omd_ca. rewrite [omd a' c']omd_reflexivity [omd c' a']/omd/omd_v c'_eq. rewrite omd_ca mulrDl mulrDl. rewrite [X in _ == X/_]mulrDl [X in _ == X]mulrDl. rewrite addrC mulrAC mulrC mulrA mulrA -mulrA divff ?omd_eq0 //. rewrite mulr1 mulrC divff; last by rewrite invr_eq0 betR_neq0. rewrite eq_sym. rewrite addrC mulrAC mulrC mulrA mulrA -mulrA divff ?omd_eq0 //. rewrite mulr1 mulrC divff ; last by rewrite invr_eq0 betR_neq0. rewrite add2r_eq. rewrite mulrAC mulrC mulrA mulrA [_^-1*_]mulrC. rewrite eq_sym. by rewrite [X in X == _]mulrAC mulrC !mulrA [_^-1*_]mulrC. rewrite -subr_eq0 opprK => /negPn /negPf H1. move: H1. rewrite lt0r_neq0 //. rewrite addr_gt0 ?mulr_gt0 ?invr_gt0 ?omd_gt0 //. move: betS_abc => /betSP[] //. move: betS_a'b'c' => /betSP[] //. have : dist a c == dist a' c' by rewrite dist_cong' (@segment_addition' a b c a' b' c') -?dist_cong' /bet'/bet ?betS_abc ?betS_a'b'c' ?orbT ?dist_ab ?dist_bc. move=> /eqP dist_ac. rewrite (@five_segment_aux5 a b c l) ; rewrite ?c_eq ?invr_eq0 ?betR_neq0 //. rewrite (@five_segment_aux5 a' b' c' l') ; rewrite ?c'_eq ?invr_eq0 ?betR_neq0 //. by rewrite dist_ab dist_ac eqxx. move:betS_a'b'c'. by rewrite betS_neq12 -point_vector_neq=> /andP [_ ]. move:betS_a'b'c'. by rewrite betS_neq13 -point_vector_neq=> /andP [_ ]. move:betS_abc. by rewrite betS_neq12 -point_vector_neq=> /andP [_ ]. move:betS_abc. by rewrite betS_neq13 -point_vector_neq=> /andP [_ ]. move=> /eqP ->. rewrite [(_^+2 * _)^-1]invfM mulrA mulrA. rewrite mulrACA -[dist a d * mu ^+ 2 / mu ^+ 2]mulrA divff; last by rewrite expr2 mulf_neq0. rewrite eq_sym. rewrite [(_^+2 * _)^-1]invfM mulrA mulrA. rewrite [X in X == _]mulrAC mulrC. rewrite mulrA mulrA mulrCA [_^-2 * _^+2]mulrC divff; last by rewrite expr2 mulf_neq0. by rewrite dist_ad dist_bd dist_ab eqxx. 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