proposition: Theorem getRzMinSym : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (a : rZ), getRzMin Ar1 Ar2 a = getRzMin Ar2 Ar1 a.
proof: Proof. intros Ar1 Ar2 War1 War2 a; case a; simpl in |- *; intros a'; rewrite getEquivMinSym; auto with stalmarck. Qed.