proposition: Lemma det_alternate (p q : Plane) : det p p q = 0.
proof: Proof. apply/eqP; rewrite -[_ == 0]/(false || _) . have<-: (2%:R : R) == 0 = false by rewrite pnatr_eq0. by rewrite -mulf_eq0 mulr_natl 2!det_cyclique mulr2n {2}det_inverse subrr. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)