proposition: Lemma extension_col a b c k : c == extension a b k -> bet a b c \/ bet b c a \/ bet c a b.
proof: Proof. rewrite /extension; case: (k =P 0)=> [->|/eqP k_neq0]. by rewrite invr0 scale0r add0r=> /eqP ->; rewrite bet_axx /=; auto. move: k_neq0=> /lt_total /orP[k_lt0|k_gt0] /eqP c_def. suffices: (bet c a b) by auto. set k' := k / (k - 1). have: (c == extension b a k')=> [|/eqP ->]; [|rewrite bet_sym]. rewrite c_def /extension /k' invf_div mulrBl divff ?ltr0_neq0 //. rewrite eq_sym scalerBl scale1r addrAC -!addrA addrC !addrA. by rewrite [-b + b]addrC subrr add0r -scalerN opprB mul1r eqxx. have: (k < 1)=> [|k_lt1]; first by apply: (@lt_trans _ _ 0); rewrite ?ltr01 //. rewrite extension_bet ?/k' // ?nmulr_rgt0 ?invr_lt0 ?subr_lt0 // -1?subr_gt0. have: (1 == (k - 1) / (k - 1)) by rewrite divff ?ltr0_neq0 ?subr_lt0 //. move=> /eqP {1}->; rewrite -mulrBl addrAC subrr add0r mulNr -mulrN. by rewrite mulr_gt0 ?ltr01 // oppr_gt0 invr_lt0 subr_lt0. move: c_def; case: (k =P 1)=> [->|/eqP k_neq1 c_def]. by rewrite invr1 scale1r addrAC addrK=> ->; rewrite bet_axx; auto. move: k_neq1=> /lt_total /orP[k_lt1|k_gt1]. by rewrite c_def extension_bet; auto. suffices: (bet b c a) by auto. set k' := k^-1; have: (c == contraction a b k'). by rewrite c_def /extension /contraction /k' eqxx. by move=> /eqP ->; rewrite bet_sym contraction_bet ?/k' ?invr_gt0 ?invf_lt1. 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