proposition: Lemma fincP (f: Tf) : (forall n, f n < f n.+1) -> (forall n m, (n < m)%N -> f n < f m).
proof: Proof. move => h n; elim => //. move => m Hm;rewrite ltnS leq_eqVlt; case /orP;first by move => /eqP ->. move /Hm => sa; exact: (T3lt_trans sa (h m)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)