proposition: Lemma proper_caseZ_diff_CS : forall (S : CSetoid) (f : nat -> nat -> S), (forall m n p q : nat, m + q = n + p -> f m n [=] f p q) -> forall m n : nat, caseZ_diff (m - n) f [=] f m n.
proof: Proof. intro CS. intros. pattern m, n in |- *. apply nat_double_ind. intro. replace (0%nat - n0)%Z with (- n0)%Z;auto. rewrite caseZ_diff_Neg; reflexivity. intros. replace (S n0 - 0%nat)%Z with (S n0:Z);auto. rewrite caseZ_diff_Pos; reflexivity. intros. generalize (H (S n0) (S m0) n0 m0); intro. cut (S n0 + m0 = S m0 + n0). intro. generalize (H1 H2); intro. apply eq_transitive with (f n0 m0). apply eq_transitive with (caseZ_diff (n0 - m0) f);auto. replace (S n0 - S m0)%Z with (n0 - m0)%Z. apply eq_reflexive. repeat rewrite Znat.inj_S; clear H1; auto with zarith. now apply eq_symmetric. clear H1; auto with zarith. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid