proposition: Theorem getRzMinMin : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (a c : rZ), rZlt c (getRzMin Ar1 Ar2 a) -> ~ (In c (getEquivList Ar1 a) /\ In c (getEquivList Ar2 a)).
proof: Proof. intros Ar1 Ar2 War1 War2 a c; case a; intros a'; generalize (getEquivMinMin Ar1 Ar2 War1 War2 a'); simpl in |- *; auto with stalmarck. case (getEquiv Ar1 a'); case (getEquiv Ar2 a'); intros l b l0 b0; case b; case b0; simpl in |- *; intros H' H'0; red in |- *; intros H'1; Elimc H'1; intros H'1 H'2; (case (H' (rZComp c)); [ apply rZltEqComp with (1 := H'0); auto with stalmarck | idtac ]); split; try apply in_map; auto with stalmarck; apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. Qed.