proposition: Lemma hcons_mult_S2 n : forall h i s s' , S2 n s s' -> S2 n (hcons_mult h i s) (hcons_mult h i s').
proof: Proof. induction i. - now simpl. - right;auto. 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)