proposition: Lemma L_succ_ok : L_spec (succ beta) L_succ.
proof: Proof. inversion_clear f_ok. - unfold L_succ; right. + discriminate. + intros; rewrite H; simpl;red; rewrite interval_singleton; left. * discriminate. * split. -- discriminate. -- reflexivity. - unfold L_succ; right. + apply succ_not_zero. + intro k; red. path_decompose (S k). instantiate (1 := beta). -- apply H0. -- rewrite interval_singleton; left. ++ discriminate. ++ split. ** apply succ_not_zero. ** now rewrite canon_succ. -- apply Nat.lt_le_pred. generalize (f_Sle (S (S k))); abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)