proposition: Lemma subr_gtlex0 (p q : Plane) : ((0%:R : R *l R) < q-p) = ((p : R *l R) < q).
proof: Proof. rewrite/lt/=/ProdLexiOrder.lt; congr (_ && (_ ==> _)). - by rewrite subr_ge0. - by rewrite subr_le0. - by rewrite subr_gt0. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)