proposition: Lemma pow_mono : monotone pow.
proof: Proof. move=>m n; elim: n m=>[|n IH] m /=; first by case: m. rewrite {1}/Poset.leq /= leq_eqVlt ltnS. case/orP; first by move/eqP=>->. move/IH=>{IH} H; apply: poset_trans H _. by elim: n=>[|n IH] //=; apply: cont_mono IH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)