proposition: Lemma size_c a b c n d: (size c < size (cons a b c n d))%N.
proof: Proof. by rewrite /= ltnS maxnC - maxnA maxnC - !maxnA leq_maxl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)