proposition: Remark R2 : gnawS alpha B1 = T1.zero.
proof: Proof. assert (H: sorted_ge 0 B1) by (eapply sorted_ge_prefix; eauto). specialize (Lemma_4_5_1 0 alpha Halpha _ _ HAB1 H HA). rewrite R1. intro H0; now rewrite (const_pathS_eps_zero H0). Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)