proposition: Theorem getRzMinUnique : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S1 S2 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> forall a b : rZ, eqStateRz S1 a b -> eqStateRz S2 a b -> getRzMin Ar1 Ar2 a = getRzMin Ar1 Ar2 b.
proof: Proof. intros Ar1 Ar2 War1 War2 S1 S2 H' H'0 a b H'1 H'2. cut (getEquivList Ar1 a = getEquivList Ar1 b); [ intros Eq1 | case (getEquivListProp4 Ar1 War1 S1 H' a b) ]; auto with stalmarck. cut (getEquivList Ar2 a = getEquivList Ar2 b); [ intros Eq2 | case (getEquivListProp4 Ar2 War2 S2 H'0 a b) ]; auto with stalmarck. case (rZltEDec (getRzMin Ar1 Ar2 a) (getRzMin Ar1 Ar2 b)); intros s; [ Casec s; intros s | idtac ]. case getRzMinMinEq with (5 := s) (S1 := S1) (S2 := S2); auto with stalmarck; split; auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply getRzMinEq1; auto with stalmarck. apply eqStateRzTrans with (b := a); auto with stalmarck. apply getRzMinEq2; auto with stalmarck. case getRzMinMinEq with (5 := s) (S1 := S1) (S2 := S2); auto with stalmarck; split; auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. apply getRzMinEq1; auto with stalmarck. apply eqStateRzTrans with (b := b); auto with stalmarck. apply getRzMinEq2; auto with stalmarck. apply OlistIn with (ltA := rZlt) (eqA := eqRz) (L := getEquivList Ar1 b); auto with stalmarck. rewrite <- Eq1. apply getRzMinIn1; auto with stalmarck. apply getRzMinIn1; auto with stalmarck. apply getEquivListProp2; auto with stalmarck. Qed.