proposition: Lemma bet_inner_transitivity a b c d: bet a b d -> bet b c d -> bet a b c.
proof: Proof. rewrite {2}/bet /betE. case: (c =P d)=> [-> //|?]. rewrite {1}/bet bet_betE. rewrite /betE; case: (b =P c)=> [->|?]; rewrite ?orbT ?orTb // andbF !orFb. case: (a =P b)=> [->|?]; rewrite ?orTb ?orbT // andFb !orFb. case: (b =P d)=> [->|?]; rewrite ?subrr ?betS_id // orFb. by move=> bet1 bet2; rewrite /bet (@betS_inner_transitivity a b c d) ?orbT. 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