proposition: Lemma lqt13 a b c : a <= b < c -> a < c.
proof: Proof. by case/andP; apply: leq_ltn_trans. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)