proposition: Theorem getRzMinMinEq : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S1 S2 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> forall a c : rZ, rZlt c (getRzMin Ar1 Ar2 a) -> ~ (eqStateRz S1 a c /\ eqStateRz S2 a c).
proof: Proof. intros Ar1 Ar2 War1 War2 S1 S2 H' H'0 a c; case a; intros a'; generalize (getEquivMinMinEq Ar1 Ar2 War1 War2 S1 S2 H' H'0 a'). auto with stalmarck. intros H'1 H'2; red in |- *; intros H'3; Elimc H'3; intros H'3 H'4. case (H'1 (rZComp c)); [ apply rZltEqComp with (1 := H'2); simpl in |- *; auto with stalmarck | idtac ]; split; auto with stalmarck. Qed.