proposition: Lemma L03 alpha n beta p : alpha <> zero -> (cons alpha n beta * FS p) = cons alpha (p + n * S p) beta.
proof: Proof. simpl. destruct alpha. now destruct 1. trivial. 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)