proposition: Lemma detD (p q r : Plane) : det 0 p (q+r) = det 0 p q + det 0 p r.
proof: Proof. by rewrite 3!det_scalar_productE /scalar_product/=; ring. Qed.
imports: encompass conv mathcomp(all_ssreflect all_algebra vector reals normedtype) mathcomp(classical_sets boolp mathcomp_extra) counterclockwise mathcomp.algebra_tactics(ring) mathcomp.zify(zify)