proposition: Remark Rem05 : ~ P t.
proof: Proof. unfold P. enough (compare (standard_gnaw (S n) alpha t) beta = Datatypes.Lt) by congruence. apply compare_lt_iff. destruct Rem03; tauto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)