proposition: Theorem addEqComp : forall (a b a' b' : rZ) (S : State), eqStateRz S a a' -> eqStateRz S b b' -> eqState (addEq (a, b) S) (addEq (a', b') S).
proof: Proof. intros a b a' b' S H' H'0. red in |- *; split; apply inclStateIn; simpl in |- *; (intros a0 b0 H'1; Elimc H'1; intros H'1; [ inversion H'1 | idtac ]); auto with stalmarck; rewrite <- H1; rewrite <- H0. apply eqStateRzTrans with (b := a'); auto with stalmarck. apply eqStateRzTrans with (b := b'); auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. Qed.
imports: Coq(List)