proposition: Theorem getMinInvInd : forall L1 L2 : list rZ, OlistRz L1 -> OlistRz L2 -> getMinInv L1 (map rZComp L2) = getMinId L1 L2.
proof: Proof. intros L1 L2 Ol1 Ol2; auto with stalmarck. cut (OlistRz (map rZComp L2)); [ intros Ol2' | red in |- *; apply Olistf with (eqA := eqRz); auto with stalmarck; exact rZltEqComp ]. CaseEq (getMinInv L1 (map rZComp L2)); auto with stalmarck. CaseEq (getMinId L1 L2); auto with stalmarck. intros x H' x0 H'0. case (rZltEDec x0 x); intros s; [ Casec s; intros s | idtac ]. absurd (x0 = x0); auto with stalmarck. unfold getMinId in H'; apply getMinMin with (10 := H'); auto with stalmarck. intros a b H'1; rewrite H'1; auto with stalmarck. unfold getMinInv in H'0; apply geMinIn with (4 := H'0); auto with stalmarck. unfold getMinInv in H'0; elim getMinComp with (4 := H'0); auto with stalmarck. intros x1 H'1; Elimc H'1; intros H'1 H'2; rewrite H'1. apply inMapComp; rewrite <- rZCompInvol; auto with stalmarck. absurd (x = rZComp (rZComp x)); auto with stalmarck. unfold getMinInv in H'0; apply getMinMin with (10 := H'0); auto with stalmarck. intros a b H'1; rewrite H'1; auto with stalmarck. unfold getMinId in H'; apply geMinIn with (4 := H'); auto with stalmarck. apply in_map; auto with stalmarck. unfold getMinId in H'; elim getMinComp with (4 := H'); auto with stalmarck. intros x1 H'1; Elimc H'1; intros H'1 H'2; rewrite H'1; auto with stalmarck. rewrite (OlistIn _ rZlt eqRz) with (a := x0) (b := x) (L := L1); auto with stalmarck. unfold getMinInv in H'0; apply geMinIn with (4 := H'0); auto with stalmarck. unfold getMinId in H'; apply geMinIn with (4 := H'); auto with stalmarck. intros H' x H'0; absurd (x = x); auto with stalmarck. unfold getMinId in H'; apply getMinNone with (8 := H'); auto with stalmarck. intros a b H'1; rewrite H'1; auto with stalmarck. unfold getMinInv in H'0; apply geMinIn with (4 := H'0); auto with stalmarck. apply inMapComp; auto with stalmarck. unfold getMinInv in H'0; elim getMinComp with (4 := H'0); auto with stalmarck. intros x0 H'1; Elimc H'1; intros H'1 H'2; rewrite H'1; rewrite <- rZCompInvol; auto with stalmarck. CaseEq (getMinId L1 L2); auto with stalmarck. intros x H' H'0. absurd (x = rZComp (rZComp x)); auto with stalmarck. unfold getMinInv in H'0; apply getMinNone with (8 := H'0); auto with stalmarck. intros a b H'1; rewrite H'1; auto with stalmarck. unfold getMinId in H'; apply geMinIn with (4 := H'); auto with stalmarck. apply in_map; auto with stalmarck. unfold getMinId in H'; elim getMinComp with (4 := H'); auto with stalmarck. intros x0 H'1; Elimc H'1; intros H'1 H'2; rewrite H'1; auto with stalmarck. Qed.