proposition: Lemma multE5 a n b a' n' b' : a' <> T1.zero -> Epsilon0.T1.T1mul (T1.cons a n b) (T1.cons a' n' b') = T1.cons (T1.T1add a a') n' (T1.T1mul (T1.cons a n b) b').
proof: Proof. move => Ha'; cbn; case: a; move: Ha'; case: a' => //. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)