proposition: Lemma col_2D_aux a b c : ((a 0 0 - b 0 0) * (b 0 1 - c 0 1) == (a 0 1 - b 0 1) * (b 0 0 - c 0 0)) -> c 0 0 != a 0 0 \/ c 0 1 != a 0 1 -> a 0 0 != b 0 0 \/ a 0 1 != b 0 1 -> b 0 0 != c 0 0 \/ b 0 1 != c 0 1 -> [ \/ [ /\ b 0 0 = a 0 0, c 0 0 = a 0 0, a 0 1 - b 0 1 != 0, b 0 1 - c 0 1 != 0 & c 0 1 - a 0 1 != 0], [ /\ b 0 1 = a 0 1, c 0 1 = a 0 1, a 0 0 - b 0 0 != 0, b 0 0 - c 0 0 != 0 & c 0 0 - a 0 0 != 0] | [ /\ [ /\ a 0 0 - b 0 0 != 0, b 0 0 - c 0 0 != 0 & c 0 0 - a 0 0 != 0] & [ /\ a 0 1 - b 0 1 != 0, b 0 1 - c 0 1 != 0 & c 0 1 - a 0 1 != 0]]].
proof: Proof. rewrite !subr_eq0; case: (a 0 0 =P b 0 0)=> [->|? /=]. rewrite subrr mul0r eq_sym mulf_eq0 !subr_eq0=> /orP[/eqP->|/eqP->]; rewrite ?eqxx /=; move=> [?|?] [?|?] [?|?] //; apply Or31; apply And5 => //; by rewrite eq_sym. case: (a 0 1 =P b 0 1)=> [->|? /=]; rewrite ?subrr ?mul0r ?mulf_eq0. rewrite !subr_eq0=> /orP[/eqP ? //|/eqP-> /=]; rewrite eqxx /=. move=> [?|//] _ [?|//]; apply Or32; apply And5 => //; by rewrite eq_sym. case: (b 0 0 =P c 0 0)=> [->|?] /=; rewrite ?subrr ?mulr0 ?mulf_eq0. rewrite !subr_eq0; move=> /orP[/eqP->|/eqP->]; move=> [/eqP ?|?] _ [?|/eqP ?]; move=> //; apply Or31; apply And5=> //; by [rewrite eq_sym|apply /eqP]. case: (b 0 1 =P c 0 1)=> [->|?] /=; rewrite ?subrr ?mulr0 eq_sym. rewrite mulf_eq0 !subr_eq0; move=> /orP[/eqP->|/eqP ? //] [?|/eqP ? //] _ _. by apply Or32; apply And5=> //; rewrite eq_sym. case: (c 0 0 =P a 0 0)=> [->|?] /=; [|case: (c 0 1 =P a 0 1)=> [->|?] /=]. rewrite -[X in _ == X *_]opprB mulNr -addr_eq0 mulrC -mulrDr mulf_eq0. rewrite addrBDB !subr_eq0 [X in X || _]eq_sym [X in _ || X]eq_sym. move=> /orP[/eqP //|/eqP ?] [/eqP //|/eqP //]. rewrite -[X in _ == _ * X]opprB mulrN -addr_eq0 mulrC -mulrDl mulf_eq0. rewrite addrC addrBDB !subr_eq0 eq_sym. move=> /orP[/eqP ?|/eqP //] [/eqP //|/eqP //]. by move=> _ _ _ _; apply Or33. 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