proposition: Lemma ap_nat_tight0 : forall x y : nat, Not (x{#N}y) <-> x = y.
proof: Proof. intros x y. red in |- *. split. unfold ap_nat in |- *. intro H. case (eq_nat_dec x y). intro e. assumption. intro n. elim H. intro H0. elim n. assumption. intro H. unfold ap_nat in |- *. intro H0. elim H0. assumption. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)