proposition: Remark Rem06 : (0 < t)%nat.
proof: Proof. generalize Rem03; destruct t. - simpl; intro; destruct (@LT_irrefl alpha). apply LT_trans with beta;auto. eapply const_pathS_LT; eauto. - auto with arith. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)