proposition: Theorem Axiom5 t s p q r : OT t s p -> OT t s q -> OT t s r -> OT t p q -> OT t q r -> OT t p r.
proof: Proof. rewrite /OT /ccw => tsp tsq tsr tpq tqr. have->: det t p r = - det t r p by rewrite !develop_det; ring. rewrite ltNge oppr_le0; apply /negP=>trp. suff: 0 < det t q r * det t s p + det t r p * det t s q + det t p q * det t s r. by rewrite convex_combination ltxx. rewrite addrC. apply ltr_paddr; [| by apply mulr_gt0]. by apply addr_ge0; apply mulr_ge0=>//; apply ltW. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)