proposition: Lemma euclid' a b c d t (k1 := betR a d t) (k2 := betR b d c) : betS a d t -> bet b d c -> exists x y, bet a b x /\ bet a c y /\ bet x t y.
proof: Proof. case: (b =P c)=> [-> betS_adt|/eqP bc_neq betS_adt bet_bdc]. by rewrite bet_xax=> /eqP ->; exists t, t; rewrite bet_xxa /bet betS_adt orbT. set x:=extension a b k1; set y:=extension a c k1; exists x, y. have: (t == extension a d k1); [|move/betSP: betS_adt =>[_ k1_gt0 k1_lt1]]. move: betS_adt; rewrite betS_neq12 /betS /betR=> /andP[/andP[/eqP ? _] ?]. by apply /eqP; rewrite /k1 /betR extensionP. by move=> /eqP t_def; rewrite !extension_bet // t_def /x /y euclid''. 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