proposition: Lemma largeb_Sb alpha s : largeb alpha s = largeSb alpha (unshift s).
proof: Proof. unfold largeb, largeSb; now rewrite gnaw_gnawS. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)