proposition: Lemma nat_compare_equiv n m : (n ?= m) = nat_compare_alt n m.
proof: Proof. unfold nat_compare_alt; destruct lt_eq_lt_dec as [[|]|]. - now apply Nat.compare_lt_iff. - now apply Nat.compare_eq_iff. - now apply Nat.compare_gt_iff. Qed.
imports: PeanoNat Decidable