proposition: Lemma L05 a n b c p d : a <> zero -> c <> zero -> (cons a n b * cons c p d) = cons (a + c) p (cons a n b * d).
proof: Proof. simpl. destruct a, c; intros. now destruct H. now destruct H. now destruct H0. auto. 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)