proposition: Lemma hcons_mult_app : forall (h: Hydra) (n :nat) (s s': Hydrae), hcons_mult h n (hy_app s s') = hy_app (hcons_mult h n s) s'.
proof: Proof. induction n. - now cbn. - cbn; intros; now rewrite IHn. Qed.
imports: Coq(Arith Lia List Relation_Operators Operators_Properties Peano_dec Wellfounded.Inverse_Image Wellfounded.Inclusion) hydras(More_Arith Epsilon0 Hessenberg Simple_LexProd MoreLibHyps)