proposition: Lemma bet_inner_transitivity : bet_inner_transitivityP Point bet'.
proof: Proof. move=> a b c d /andP[Hb1 /implyP Himp1] /andP[Hb2 _]. rewrite /bet' (bet_inner_transitivity Hb1 Hb2) /=; apply /implyP. move=> /and3P[/eqP E1 /eqP E2 /eqP E3]; case: (b =P c)=> [//|bc_neq]. have E4 : (d 0 1 = 0) by apply (bet_on_abscissa bc_neq)=> //; rewrite -E1. have E5 : (b = d) by apply /eqP; apply Himp1; rewrite E2 E1 E4 !eqxx. by exfalso; apply bc_neq; apply /eqP; rewrite -E5 in Hb2; rewrite -bet_xax. 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) mathcomp(zmodp) GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence