proposition: Theorem stalmarckGivesValidEquation : forall (L : list triplet) (a b : rZ) (S : State), stalmarckP (addEq (a, rZComp b) nil) L S -> contradictory S -> validEquation L a b.
proof: Proof. intros L a b S H' H'0. red in |- *; auto with stalmarck. intros f H'1 H'2; case (boolDec (rZEval f a) (rZEval f b)); auto with stalmarck. intros H'3; absurd (realizeState f S); auto with stalmarck. apply stalmarckRealizeStateEval with (S1 := addEq (a, rZComp b) nil) (L := L); auto with stalmarck. apply realizeStateAddEq; auto with stalmarck. rewrite rZEvalCompInv; generalize H'3; case (rZEval f a); case (rZEval f b); auto with stalmarck; intros H'4; case H'4; auto with stalmarck. Qed.