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