proposition: Lemma det0_aligned (p q r: Plane) : det p q r = 0%R <-> (p = q \/ exists t, p <| t |> q = r).
proof: Proof. rewrite det_scalar_productE. symmetry; split. case. by move=>->; rewrite subrr -(scaler0 _ 0) scalar_productZL mul0r. by move=> [t <-]; rewrite convlr addrAC subrr add0r rotateZ scalar_productZR scalar_product_rotatexx mulr0. wlog: p q r / p == 0%R. move=> h; rewrite -[q-p]subr0 -[r-p]subr0. move=>/(h 0%R (q-p) (r-p) (eqxx 0%R)); case=>[ /eqP | [t] ]. by rewrite eq_sym subr_eq0 eq_sym=>/eqP=>pq; left. by rewrite{1}/conv scaler0 add0r=>/(f_equal (fun x=> p+x)); rewrite [r-p]addrC addrA subrr add0r=><-; right; exists t=>//; apply convlr. move=>/eqP p0; subst p; rewrite !subr0/scalar_product/= mulrN=>/eqP; rewrite subr_eq0=>/eqP e. have [q0|q0] := eqVneq q 0%R; first by left. right. move:q0; rewrite -pair_eqE /= negb_and => /orP[|] q0. exists (1 - xcoord r / xcoord q)=>//. rewrite -convC convrl add0r subr0; apply /eqP; rewrite -pair_eqE; apply /andP; split=>/=; have ->: forall (a: R) (b: (regular_vectType (Real.ringType R))), a *: b = a*b by lazy. - by rewrite -mulrA [_^-1*_]mulrC divff // mulr1. - by rewrite mulrC mulrA -e mulrC mulrA [_^-1*_]mulrC divff // mul1r. exists (1 - ycoord r / ycoord q)=>//. rewrite -convC convrl add0r subr0; apply /eqP; rewrite -pair_eqE; apply /andP; split=>/=; have ->: forall (a: R) (b: regular_vectType (Real.ringType R)), a *: b = a*b by lazy. - by rewrite mulrC mulrA e mulrC mulrA [_^-1*_]mulrC divff // mul1r. - by rewrite -mulrA [_^-1*_]mulrC divff // mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg matrix ssrnum vector reals normedtype order boolp classical_sets) counterclockwise