proposition: Lemma T1le_cons_le a n b a' n' b': (cons a n b <= cons a' n' b') -> (a <= a').
proof: Proof. case /orP; [ by case /eqP => -> | apply:T1lt_cons_le ]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)