proposition: Lemma T1mul_cons_cons_E n b n' b' : cons zero n b * cons zero n' b' = cons zero (n * n' + n + n') b'.
proof: Proof. done. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)