proposition: Lemma L5 a n b c p : a <> zero -> c <> zero -> (cons a n b) * (cons c p zero) = cons (a + c) p zero.
proof: Proof. cbn; destruct a,c; trivial. - now destruct 1. - now destruct 2. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)