proposition: Lemma decompose_det (p q r t : Plane) : det p q r = (det t q r) + (det p t r) + (det p q t).
proof: Proof. by rewrite !develop_det; ring. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)