proposition: Lemma five_segment a a' b b' c c' d d' : cong a b a' b' -> cong b c b' c' -> cong a d a' d' -> cong b d b' d' -> bet a b c -> bet a' b' c' -> a <> b -> cong c d c' d'.
proof: Proof. move=> c1 c2 c3 c4 /orP[/betEP[[->->]|->|E]|b1 /orP[/betEP[[E _]|E|E]|b2]]=> //; try solve[rewrite E in c2; apply cong_eq' in c2; move=> _ _; rewrite -c2 -E //]; try solve[rewrite -E in c1; apply cong_eq in c1; rewrite -c1 //]; try solve[rewrite -E in c2; apply cong_eq in c2; rewrite -c2 -E //]. move: c1 c2 c3 c4; rewrite congC /cong=> /eqP c1 /eqP c2 /eqP c3 /eqP c4 _. rewrite (cosine_rule b) c2 c4 [X in _ == X](cosine_rule b') -!addrA !add2r_eq. rewrite (betS_ratio b1) (betS_ratio b2) -!scalemxAl -!scalerAr !cosine_rule'. by rewrite (bet_cong_ratio_eq b1 b2) /cong ?c1 ?c2 ?c3 ?c4. 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