proposition: Lemma add_to_cons a b n c: c < [a,b] -> cons a b n zero + c = cons a b n c.
proof: Proof. case: c => // u v m z /=; rewrite T2lt_consE - T2lt_psi T2ltn0 !if_same. by rewrite if_simpl => h; rewrite h (T2lt_anti h). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)