proposition: Remark R22 : delta = standard_gnaw (S n) alpha (S l).
proof: Proof. replace (S l) with (l + 1)%nat;[| lia]. rewrite standard_gnaw_plus. fold gamma. simpl; replace (l + S n)%nat with (S (n+l)); [trivial | lia]. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)