proposition: Lemma f_elim' : forall (P : nat -> nat -> Prop), P 10 0 -> (forall (x : nat) (H : discr_10 x), P x (x + 1)) -> (forall n : nat, P n (f n)).
proof: Proof. intros. apply (f_elim P (fun x H r => P x r)); auto. Defined.
imports: Equations(Equations) Coq(List Program.Syntax Arith Lia)