proposition: Lemma R_nat_elaguee_domain : forall y n, R y n -> exists p, R_nat_elaguee y p.
proof: Proof. assert (forall (n : nat) (y : A), (exists q:nat, q <= n /\ R y q) -> exists p : nat, R_nat_elaguee y p). induction n. intros y (q,(H1,H2)). exists 0. split; auto with arith. inversion H1. subst q; auto. intros y (q,(H1,H2)). case (classic (exists r, r <= n /\ R y r)). intro H';case (IHn y H'). intros;exists x;auto. exists q. split. auto. intros. case (Compare_dec.le_lt_dec q p). auto. intro. case H. exists p. split;auto with arith. lia. intros. eapply H with n. exists n;auto with arith. Qed.
imports: Coq(Ensembles Classical Lia Arith) hydras(PartialFun)