proposition: Lemma hcons_mult_comm : forall i h s, hcons_mult h i (hcons h s) = hcons h (hcons_mult h i s).
proof: Proof. induction i as [| i IHi]; simpl; auto. intros; now rewrite IHi. 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)