proposition: Lemma multE4 a n b n' b' : a <> Epsilon0.T1.zero -> Epsilon0.T1.T1mul (T1.cons a n b) (T1.cons Epsilon0.T1.zero n' b') = T1.cons a (n * n' + n + n') b.
proof: Proof. cbn; case: a => [// | a n0 ? _ ]; congr T1.cons; nia. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)