proposition: Lemma remove_heads_r_free: forall i h j, rounds free j (add_r h (S i)) (S i+j)%nat h.
proof: Proof. intros; specialize (remove_heads_r i h j). induction 1. left. now apply standard_incl_free. auto. right with h''. now apply standard_incl_free. 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)