proposition: Lemma beq_nat_eq_nat_dec : forall x y, Nat.eqb x y = if eq_nat_dec x y then true else false.
proof: Proof. intros; destruct (eq_nat_dec _ _); [ apply Nat.eqb_eq | apply Nat.eqb_neq ]; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith