proposition: Theorem getMinMin : forall (L1 L2 : list A) (a : A), Olist L1 -> Olist L2 -> getMin L1 L2 = Some a -> forall b c : A, ltA b a -> In b L1 -> In c L2 -> ~ test b c.
proof: Proof. intros L1; elim L1; simpl in |- *. intros L2; case L2; simpl in |- *; auto with datatypes core. intros a l H' L2; case L2; simpl in |- *; auto with datatypes core. intros a0 l0 a1 H'0 H'1. case (ltADec a a0); intros s; auto. Casec s; intros s; auto. intros H'2 b c H'3 H'4 H'5; Casec H'4; intros H'4; auto. rewrite <- H'4; auto. red in |- *; intros H'6; absurd (In c (a0 :: l0)); auto. apply OlistUnique with (a := a); auto. apply (H' (a0 :: l0) a1); auto. apply OlistInv with (a := a); auto. generalize H'1; elim l0; auto. intros H'2 H'3; discriminate. intros a2 l1 H'2 H'3. case (ltADec a a2); intros s1; auto. Casec s1; intros s1; auto. intros H'4 b c H'5 H'6 H'7; Casec H'6; intros H'6; auto. rewrite <- H'6; auto. Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto. red in |- *; intros H'8; absurd (eqA a0 a); auto. red in |- *; intros H'8; absurd (In c (a2 :: l1)); auto. apply OlistUnique with (a := a); auto. apply OlistCons; auto. apply OlistInv with (a := a0); auto. Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto. red in |- *; intros H'8; Contradict H'6; auto. apply OlistUnique with (a := a0); auto. apply OlistSkip with (b := a); auto. apply (H' (a2 :: l1) a1); auto. apply OlistInv with (a := a); auto. apply OlistInv with (a := a0); auto. simpl in |- *; intros H'4 b c H'5 H'6 H'7; auto. Casec H'7; intros H'7; auto. apply (H'2 (OlistSkip _ _ _ H'3) H'4); auto. Casec H'7; intros H'7; auto. rewrite <- H'7. Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto. red in |- *; intros H'8; absurd (eqA a2 a); auto. Contradict H'6. apply OlistUnique with (a := a2); auto. apply OlistSkip with (b := a); auto. apply (H'2 (OlistSkip _ _ _ H'3) H'4); auto. case (testDec a a2 s1); auto. intros H'4 H'5; inversion H'5; auto. rewrite <- H0. intros b c H'6 H'7 H'8; absurd (In b (a :: l)); auto. apply OlistUnique with (a := b); auto. intros H'4 H'5 b c H'6 H'7 H'8. Elimc H'8; simpl in |- *; intros H'8. apply (H'2 (OlistSkip _ _ _ H'3) H'5); auto. Elimc H'8; simpl in |- *; intros H'8. rewrite <- H'8. Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto. Contradict H'7; auto. apply OlistUnique with (a := a); auto. apply eqATrans with a2; auto. apply (H'2 (OlistSkip _ _ _ H'3) H'5); auto. case (testDec a a0 s); auto. intros H'2 H'3; inversion H'3. intros b c H'4 H'5 H'6. Elimc H'5; intros H'5; [ rewrite <- H'5 in H'4; Contradict H'4 | idtac ]; auto. Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto. Contradict H'5. apply OlistUnique with (a := a); auto. apply eqATrans with a0; auto. Contradict H'5. apply OlistUnique with (a := b); auto. apply OlistSkip with (b := a1); auto. apply OlistCons; auto. rewrite <- H0; auto. intros H'2 H'3 b c H'4 H'5 H'6. Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto. Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto. Contradict H'5. apply OlistUnique with (a := a); auto. apply eqATrans with a0; auto. Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto. Contradict H'6. apply OlistUnique with (a := a0); auto. apply eqATrans with a; auto. apply (H' l0 a1); auto. apply OlistInv with (a := a); auto. apply OlistInv with (a := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)