proposition: Remark Rem2 : {t: nat | standard_gnaw (S n) alpha t t1< beta}.
proof: Proof. destruct (standard_gnaw_to_zero Halpha (S n)); exists x; now rewrite e. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)