proposition: Lemma decompose_base (p q : Plane) : q != 0 -> p = (scalar_product p q) / (scalar_product q q) *: q + (scalar_product p (rotate q)) / (scalar_product q q) *: rotate q.
proof: Proof. move=>q0. move: (scalar_productrr_gt0 q0)=>/lt0r_neq0 q0'. move: (q0')=>/negPf q0''. apply/eqP; rewrite -subr_eq0 -[_ == 0]/(false || _) -q0'' -scaler_eq0 scalerDr scalerN subr_eq0 /= scalerDr !scalerA !mulrA ![_ q q * _ p _]mulrC -!mulrA divff ?q0'// !mulr1 -pair_eqE /scalar_product. apply/andP; split; apply/eqP=>/=; cbn; ring. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)