proposition: Theorem getMinInvSym : forall L1 L2 : list rZ, OlistRz L1 -> OlistRz L2 -> match getMinInv L1 L2 with | None => getMinInv L2 L1 = None | Some a => getMinInv L2 L1 = Some (rZComp a) end.
proof: Proof. intros L1 L2 H' H'0; CaseEq (getMinInv L1 L2). CaseEq (getMinInv L2 L1). intros x H'1 x0 H'2. case (rZltEDec x0 x); auto with stalmarck. intros H'3; case H'3. intros H'4. absurd (rZComp x0 = rZComp x0); auto with stalmarck. unfold getMinInv in H'1; apply getMinMin with (10 := H'1); auto with stalmarck. intros a b H'5; rewrite H'5; auto with stalmarck. apply rZltEqComp with (a := x0) (b := x); auto with stalmarck. unfold getMinInv in H'2; case getMinComp with (4 := H'2); auto with stalmarck. intros x1 H'5; elim H'5; intros H'6 H'7; rewrite H'6; rewrite rZCompInv; auto with stalmarck. unfold getMinInv in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. intros H'4. absurd (rZComp x = rZComp x); auto with stalmarck. unfold getMinInv in H'2; apply getMinMin with (10 := H'2); auto with stalmarck. intros a b H'5; rewrite H'5; auto with stalmarck. apply rZltEqComp with (a := x) (b := x0); auto with stalmarck. unfold getMinInv in H'1; case getMinComp with (4 := H'1); auto with stalmarck. intros x1 H'5; elim H'5; intros H'6 H'7; rewrite H'6; rewrite rZCompInv; auto with stalmarck. unfold getMinInv in H'1; apply geMinIn with (4 := H'1); auto with stalmarck. intros H'3; rewrite (OlistIn _ rZlt eqRz) with (L := L1) (a := x0) (b := rZComp x); auto using f_equal with stalmarck. unfold getMinInv in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. unfold getMinInv in H'1; case getMinComp with (4 := H'1); auto with stalmarck. intros x1 H'5; elim H'5; intros H'6 H'7; rewrite H'6; rewrite rZCompInv; auto with stalmarck. apply eqrZTrans with (1 := H'3); auto with stalmarck. intros H'1 x H'2; absurd (rZComp x = rZComp x); auto with stalmarck. unfold getMinInv in H'1; apply getMinNone with (8 := H'1); auto with stalmarck. intros a b H'3; rewrite H'3; auto with stalmarck. unfold getMinInv in H'2; case getMinComp with (4 := H'2); auto with stalmarck. intros x1 H'5; elim H'5; intros H'6 H'7; rewrite H'6; rewrite rZCompInv; auto with stalmarck. unfold getMinInv in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. intros H'1; CaseEq (getMinInv L2 L1); auto with stalmarck. intros x H'2; absurd (rZComp x = rZComp x); auto with stalmarck. unfold getMinInv in H'1; apply getMinNone with (8 := H'1); auto with stalmarck. intros a b H'3; rewrite H'3; auto with stalmarck. unfold getMinInv in H'2; case getMinComp with (4 := H'2); auto with stalmarck. intros x1 H'5; elim H'5; intros H'6 H'7; rewrite H'6; rewrite rZCompInv; auto with stalmarck. unfold getMinInv in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. Qed.