proposition: Lemma ap_nat_irreflexive0 : forall x : nat, Not (x{#N}x).
proof: Proof. red in |- *. unfold ap_nat in |- *. intros x X. apply X. auto. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)