proposition: Lemma finite_ltP n p : (n < p)%N = (\F n < \F p).
proof: Proof. case: p => //; first by rewrite T3ltn0 ltn0. by case: n => // n p //=; rewrite T3lt_consE ltnS if_same if_simpl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)