proposition: Lemma canon_lt : forall i alpha, nf alpha -> alpha <> zero -> T1.lt (canon alpha i) alpha.
proof: Proof. intros i alpha Hnf. destruct (T1_eq_dec alpha zero). - subst. now destruct 1. - destruct (canon_LT i Hnf); tauto. Qed.
imports: hydras.Prelude(DecPreOrder)