proposition: Theorem getEquivMinMin : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (a : rNat) (c : rZ), rZlt c (getEquivMin Ar1 Ar2 a) -> ~ (In c (getEquivList Ar1 (rZPlus a)) /\ In c (getEquivList Ar2 (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). intros x H' H'0 H'1 H'2 H'3 c H'4; red in |- *; intros H'5; Elimc H'5; intros H'5 H'6. absurd (rZComp c = rZComp c); auto with stalmarck. unfold getMinId in H'; apply getMinMin with (10 := H'); auto with stalmarck. intros a0 b1 H'7; rewrite H'7; 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 rZltEqComp with (a := c) (b := rZComp x); auto with stalmarck. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. 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). intros x H' H'0 H'1 H'2 H'3 c H'4; red in |- *; intros H'5; Elimc H'5; intros H'5 H'6; auto with stalmarck. absurd (rZComp c = rZComp c); auto with stalmarck. unfold getMinInv in H'; apply getMinMin with (10 := H'); auto with stalmarck. intros a0 b1 H'7; rewrite H'7; auto with stalmarck. rewrite (rZCompInvolList l); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. apply rZltEqComp with (a := c) (b := rZComp x); auto with stalmarck. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. 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). intros x H' H'0 H'1 H'2 H'3 c H'4; red in |- *; intros H'5; Elimc H'5; intros H'5 H'6. absurd (c = rZComp (rZComp c)); auto with stalmarck. unfold getMinInv in H'; apply getMinMin with (10 := H'); auto with stalmarck. intros a0 b1 H'7; rewrite H'7; auto with stalmarck. rewrite (rZCompInvolList l0); auto with stalmarck. apply Olistf with (eqA := eqRz); auto with stalmarck. try exact rZltEqComp. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. 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). intros x H' H'0 H'1 H'2 H'3 c H'4; red in |- *; intros H'5; Elimc H'5; intros H'5 H'6. absurd (c = c); auto with stalmarck. unfold getMinId in H'; apply getMinMin with (10 := H'); auto with stalmarck. intros a0 b1 H'7; rewrite H'7; 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.