proposition: Lemma neq0 m n : m < n -> n != 0.
proof: Proof. by move/gt0; rewrite lt0n. 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)