proposition: Lemma hy_app_assoc : forall (s1 s2 s3 : Hydrae) , hy_app s1 (hy_app s2 s3) = hy_app (hy_app s1 s2) s3.
proof: Proof. induction s1. - reflexivity. - intros s2 s3; cbn; now rewrite IHs1. 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)