proposition: Lemma min_alt_correct : extEqual 2 min_alt Nat.min.
proof: Proof. intros x y. cbn. unfold leBool, ltBool. destruct (le_lt_dec x y). cbn. rewrite (PeanoNat.Nat.min_l _ _ l); ring. destruct (min_spec y x). destruct H; ring_simplify. rewrite PeanoNat.Nat.min_comm. auto. destruct H; lia. Qed.
imports: hydras(primRec extEqualNat) Coq(Compare_dec Lia ArithRing)