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