proposition: Theorem Axiom1 (p q r : Plane) : OT p q r -> OT q r p.
proof: Proof. congr (_ < _). rewrite !develop_det; ring. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)