proposition: Lemma R_nat_elaguee_fun : rel_functional DA R_nat_elaguee.
proof: Proof. intros a b b' aInDA a_Re_b a_Re_b'. destruct a_Re_b; destruct a_Re_b'. apply Nat.le_antisymm. now apply (H0 b'). now apply (H2 b). Qed.
imports: Coq(Ensembles Classical Lia Arith) hydras(PartialFun)