proposition: Theorem getMinIdSym : forall L1 L2 : list rZ, OlistRz L1 -> OlistRz L2 -> getMinId L1 L2 = getMinId L2 L1.
proof: Proof. intros L1 L2 H' H'0; CaseEq (getMinId L1 L2). CaseEq (getMinId 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 (x0 = x0); auto with stalmarck. unfold getMinId in H'1; apply getMinMin with (10 := H'1); auto with stalmarck. intros a b H'5; rewrite H'5; auto with stalmarck. unfold getMinId 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; auto with stalmarck. unfold getMinId in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. intros H'4. absurd (x = x); auto with stalmarck. unfold getMinId in H'2; apply getMinMin with (10 := H'2); auto with stalmarck. intros a b H'5; rewrite H'5; auto with stalmarck. unfold getMinId 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; auto with stalmarck. unfold getMinId in H'1; apply geMinIn with (4 := H'1); auto with stalmarck. intros H'3; rewrite (OlistIn _ rZlt eqRz) with (L := L1) (7 := H'3); auto with stalmarck. unfold getMinId in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. unfold getMinId 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; auto with stalmarck. intros H'1 x H'2; absurd (x = x); auto with stalmarck. unfold getMinId in H'1; apply getMinNone with (8 := H'1); auto with stalmarck. intros a b H'3; rewrite H'3; auto with stalmarck. unfold getMinId 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; auto with stalmarck. unfold getMinId in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. intros H'1; CaseEq (getMinId L2 L1); auto with stalmarck. intros x H'2; absurd (x = x); auto with stalmarck. unfold getMinId in H'1; apply getMinNone with (8 := H'1); auto with stalmarck. intros a b H'3; rewrite H'3; auto with stalmarck. unfold getMinId 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; auto with stalmarck. unfold getMinId in H'2; apply geMinIn with (4 := H'2); auto with stalmarck. Qed.