proposition: Lemma convex_combination p q r s t : det t q r * det t s p + det t r p * det t s q + det t p q * det t s r = 0.
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)