proposition: Lemma T1mulE4 a n b n' b' : a != zero -> (cons a n b) * (cons zero n' b') = cons a (n * n' + n + n') b.
proof: Proof. move => /T1eqP; cbn => Ha'. have Heq: T1eq a zero = false by case: a Ha' => // /=. by rewrite Heq. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0)