proposition: Theorem Axiom2 (p q r : Plane) : OT p q r -> ~ OT p r q.
proof: Proof. rewrite /OT /ccw lt0r=>/andP [_ pqr]. rewrite det_inverse oppr_gt0. by rewrite ltNge pqr. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)