proposition: Lemma LT_to_round_plus a b : b t1< a -> iota a -+-> iota b.
proof: Proof. intros H; apply acc_from_to_round_plus; eauto with T1. - intro; subst; apply (not_LT_zero H). - apply LT_acc_from; eauto with T1. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )