nat_compare n m = compare_invert (nat_compare m n).
intros.
apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)));intros
nat_compare n m = compare_invert (nat_compare m n).
intros.
apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)));intros