proposition: Theorem le_0_r : ∀ n, n ≤ 0 ↔ n = 0.
proof: Proof. intros n. split; intros Hn. destruct n as [n| ]; [ idtac | inversion Hn ]. apply fin_inj_wd. apply fin_le_mono in Hn. apply Nat.le_0_r; assumption. subst n; apply le_0_l. Qed.
imports: Utf8 Compare_dec NPeano Misc