proposition: Lemma det0_colinear (p q r : Plane) : det p q r = 0 <-> exists (t : Plane), t != 0 /\ scalar_product t q = scalar_product t p /\ scalar_product t r = scalar_product t p.
proof: Proof. rewrite det_scalar_productE; move: p q r. suff: forall p q : Plane, scalar_product p (rotate q) = 0 <-> (exists (t : Plane), t != 0 /\ scalar_product t p = 0 /\ scalar_product t q = 0). move=>h p q r; move: h=> /(_ (q-p) (r-p)) ->; split. by move=>[t [t0 ts]]; exists t; split=>//; split; apply/eqP; rewrite -subr_eq0 -mulN1r -scalar_productZR -scalar_productDr scaleN1r; apply /eqP; apply ts; rewrite !in_cons eq_refl ?orbT. by move=>[t [t0 [qp rp]]]; exists t; split=>//; rewrite -scaleN1r 2!scalar_productDr scalar_productZR mulN1r qp rp subrr. move=> p q; split. 2: by move=>[t [t0 [p0 q0]]]; rewrite (decompose_base p t0) [_ p t]scalar_productC p0 mul0r scale0r add0r scalar_productZL scalar_product_rotate q0 mulr0. move=>pq. case p0: (p == 0). move: p0=>/eqP p0; subst p. case q0: (q == 0). move: q0=>/eqP q0; subst q. exists (1, 0); split. by rewrite negb_and; apply/orP; left=>/=; apply oner_neq0. by rewrite -(scale0r (0 : Plane)) scalar_productZR mul0r. exists (rotate q); split. apply/eqP=>/pair_equal_spec [q2 /eqP]; rewrite oppr_eq0=>/eqP q1. by move: q0; rewrite -pair_eqE/pair_eq q1 q2 eq_refl. by rewrite scalar_productC [_ _ q]scalar_productC scalar_product_rotatexx. exists (rotate p); split. apply/eqP=>/pair_equal_spec [p2 /eqP]; rewrite oppr_eq0=>/eqP p1. by move: p0; rewrite -pair_eqE/pair_eq p1 p2 eq_refl. split. by rewrite scalar_productC scalar_product_rotatexx. by rewrite rotate_antisym pq oppr0. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)