proposition: Lemma if_to_min {x y} : (if x <? y then x else y) = min x y.
proof: Proof. apply min_case_strong_l; intro. { rewrite (proj2 (Nat.ltb_lt _ _)) by assumption. reflexivity. } { destruct (x <? y) eqn:H'; [ | reflexivity ]. apply Nat.ltb_lt in H'. omega. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith