proposition: Lemma minPR_correct : extEqual 2 minPR PeanoNat.Nat.min.
proof: Proof. intros a b; unfold minPR, naryIf, leBool. destruct (le_lt_dec a b). - rewrite PeanoNat.Nat.min_l; auto; reflexivity. - rewrite PeanoNat.Nat.min_r; auto with arith; reflexivity. Qed.
imports: hydras(primRec extEqualNat) Coq(ArithRing Lia Compare_dec)