proposition: Lemma size_onthPn s n : reflect (onth s n = None) (size s <= n).
proof: Proof. by rewrite leqNgt; apply: (iffP idP); case: onth_sizeP=>//= v ->. 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)