proposition: Theorem contradictoryAddEq : forall (S : State) (a b : rZ), contradictory (addEq (a, b) S) -> eqStateRz S a (rZComp b).
proof: Proof. intros S a b H'; cut (eqConstrState (addEq (a, b) S) a (rZComp a)). unfold addEq in |- *; intros H'1; inversion H'1; auto with stalmarck; try (apply eqStateRzContr with (a := a); auto with stalmarck; fail). red in H'. Elimc H'; intros a0 E. apply eqStateRzPImpeqConstrState. apply eqStateRzContr with (a := a0); auto with stalmarck. Qed.
imports: Stalmarck(stalmarck) Stalmarck(ltState)