proposition: Theorem getEquivMinMinEq : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S1 S2 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> forall (a : rNat) (c : rZ), rZlt c (getEquivMin Ar1 Ar2 a) -> ~ (eqStateRz S1 (rZPlus a) c /\ eqStateRz S2 (rZPlus a) c).
proof: Proof. intros Ar1 Ar2 War1 War2 S1 S2 H' H'0 a c H'1; red in |- *; intros H'2; Elimc H'2; intros H'2 H'3; auto with stalmarck. absurd (In c (getEquivList Ar1 (rZPlus a)) /\ In c (getEquivList Ar2 (rZPlus a))); auto with stalmarck. apply getEquivMinMin; auto with stalmarck. split; auto with stalmarck. case (getEquivListProp1 Ar1 War1 (rZPlus a) c). intros H'4 H'5; apply H'5; auto with stalmarck. apply rArrayStateDef1 with (S := S1); auto with stalmarck. case (getEquivListProp1 Ar2 War2 (rZPlus a) c). intros H'4 H'5; apply H'5; auto with stalmarck. apply rArrayStateDef1 with (S := S2); auto with stalmarck. Qed.