proposition: Lemma beq_nat_min_0 {x y} : Nat.eqb (min x y) 0 = orb (Nat.eqb x 0) (Nat.eqb y 0).
proof: Proof. destruct x, y; simpl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith