proposition: Lemma Lemma2_6_1_E0 (alpha beta: E0) : (beta o< alpha)%e0 -> {n:nat | Canon_plus (S n) alpha beta}.
proof: Proof. destruct alpha, beta; unfold E0lt; simpl. simpl. intro H; eapply Lemma2_6_1; eauto. Defined.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)