R.v

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0 
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

Require Import Omega.

Theorem R_is_plus : 
  forall m n o, 
    R m n o -> m + n = o.
Proof.
  induction 1; omega.
Qed.


Theorem foo : ~ R 2 2 6.
Proof.
  intro.
  apply R_is_plus in H.
  omega.
Qed.