proposition: Theorem Axiom4 (p q r t : Plane) : OT t q r -> OT p t r -> OT p q t -> OT p q r.
proof: Proof. rewrite /OT /ccw (decompose_det p q r t)=> tqr ptr pqt. apply addr_gt0=>//. apply addr_gt0=>//. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)