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