proposition: Lemma direct_distincts (p q r : Plane) : ccw p q r -> p <> q.
proof: Proof. move=> pqr pq; subst q; move: pqr; rewrite /ccw /det. have n: (ord0: 'I_3) != lift ord0 ord0 by apply/eqP=>e; inversion e. rewrite -det_tr (determinant_alternate n). by rewrite ltxx. by move=>i; rewrite !mxE. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)