proposition: Lemma remove_heads_r : forall i h j, rounds standard j (add_r h (S i)) (S i+j)%nat h.
proof: Proof. induction i. - simpl; intros; left;auto. simpl; replace h with (add_r h 0) at 2. + left; apply R1_remove_r_i. + now rewrite add_r_0. - intros h j; specialize (IHi h (S j)). apply rounds_trans with (S j) (add_r h (S i)). + replace (S (S i) + j)%nat with (S i + S j)%nat; auto. lia. + left. * apply round_n_remove_h. 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)