proposition: Lemma round_n_remove_h : forall i j h, round_n j (add_r h (S i)) (add_r h i).
proof: Proof. intros; left;apply R1_remove_r_i. 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)