proposition: Lemma round_plus_trans : forall h h' h'', h -+-> h' -> h' -+-> h'' -> h -+-> h''.
proof: Proof. unfold round_plus. intros h h' h''; repeat rewrite <- clos_trans_t1n_iff. econstructor 2; eauto. 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)