proposition: Theorem getEquivMinIn1 : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (a : rNat), In (getEquivMin Ar1 Ar2 a) (getEquivList Ar1 (rZPlus a)).
proof: Proof. intros Ar1 Ar2 War1 War2 a; generalize (getEquivListProp2 Ar1 War1 (rZPlus a)); generalize (getEquivListProp3 Ar1 War1 (rZPlus a)); generalize (getEquivListProp2 Ar2 War2 (rZPlus a)); generalize (getEquivListProp3 Ar2 War2 (rZPlus a)); simpl in |- *; unfold getEquivMin in |- *; case (getEquiv Ar1 a); intros l b; case b; case (getEquiv Ar2 a); intros l0 b0; case b0; auto with stalmarck. CaseEq (getMinId l l0); auto with stalmarck. intros x H' H'0 H'1 H'2 H'3; apply in_map; auto with stalmarck. unfold getMinId in H'; apply geMinIn with (4 := H'); auto with stalmarck. rewrite (rZCompInvolList l); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. rewrite (rZCompInvolList l0); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. intros H' H'0 H'1 H'2 H'3. unfold getMinId in H'; case getMinNone with (8 := H') (a := rZMinus a) (b := rZMinus a); auto with stalmarck. intros a0 b1 H'4; rewrite H'4; auto with stalmarck. rewrite (rZCompInvolList l); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. rewrite (rZCompInvolList l0); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. apply inMapComp; auto with stalmarck. apply inMapComp; auto with stalmarck. CaseEq (getMinInv l l0); auto with stalmarck. intros x H' H'0 H'1 H'2 H'3; apply in_map; auto with stalmarck. unfold getMinInv in H'; apply geMinIn with (4 := H'); auto with stalmarck. rewrite (rZCompInvolList l); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. intros H' H'0 H'1 H'2 H'3. unfold getMinInv in H'; case getMinNone with (8 := H') (a := rZMinus a) (b := rZPlus a); auto with stalmarck. intros a0 b1 H'4; rewrite H'4; auto with stalmarck. rewrite (rZCompInvolList l); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. apply inMapComp; auto with stalmarck. CaseEq (getMinInv l l0); auto with stalmarck. intros x H' H'0 H'1 H'2 H'3. unfold getMinInv in H'; apply geMinIn with (4 := H'); auto with stalmarck. rewrite (rZCompInvolList l0); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. intros H' H'0 H'1 H'2 H'3. unfold getMinInv in H'; case getMinNone with (8 := H') (a := rZPlus a) (b := rZMinus a); auto with stalmarck. intros a0 b1 H'4; rewrite H'4; auto with stalmarck. rewrite (rZCompInvolList l0); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. apply inMapComp; auto with stalmarck. CaseEq (getMinId l l0); auto with stalmarck. intros x H' H'0 H'1 H'2 H'3. unfold getMinId in H'; apply geMinIn with (4 := H'); auto with stalmarck. intros H' H'0 H'1 H'2 H'3. unfold getMinId in H'; case getMinNone with (8 := H') (a := rZPlus a) (b := rZPlus a); auto with stalmarck. intros a0 b1 H'4; rewrite H'4; auto with stalmarck. Qed.