proposition: Lemma no_inverse0 : forall f : nat -> nat, ~ ((2+f 2) = 0 /\ (f 2+2) = 0).
proof: Proof. intro f. simpl in |- *. red in |- *. intro H. elim H. intros H1 H2. set (H3 := O_S (S (f 2))) in *. generalize H3. unfold not in |- *. intro H4. apply H4. lia. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)