proposition: Lemma not_lt : forall n m, (false = (n < m)) -> (m <= n).
proof: Proof. move => n m. by elim: n m=> [| n IHn]; case. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)