proposition: Lemma five_segment : ~ five_segmentP Point bet' cong'.
proof: Proof. unfold five_segmentP=> H. set a := (@row2 R 0 1); set b := (@row2 R 1 1); set c := (@row2 R (1+1) (1+1)). set d := (@row2 R 1 (1+1)); set d' := (@row2 R 1 0); absurd (cong' c d c d'). rewrite /cong' /cong !mxE eqxx /= subrr mul0mx eq_sym quad_eq0. rewrite -[X in X == _]opprB oppr_eq0 -scalemx1 -[0%:M]scalemx1 -scalerBl. rewrite subr0 scalemx_eq0=> /orP [|/eqP HF]; rewrite ?paddr_eq0 ?oner_eq0; by rewrite ?ler01 //; move: (matrix_nonzero1 R 0); rewrite HF eqxx. apply (H a a b b c c d d'); rewrite /bet' /a /b /c /d /d'; try apply /congP; rewrite /sqr_L2_norm_1D_i /sqr_L2_norm_1D ?mxE /= ?eqxx ?bet_xxa ?andbT //=; rewrite ?mul0rn ?sub0r ?mulr1n ?sqrrN -1?addrA ?subrr ?addr0 ?eqxx ?bet_012 //. by apply /eqP; rewrite -subr_eq0 vector2_eq0 !mxE /= sub0r oppr_eq0 oner_eq0. 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.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence