proposition: Theorem getMinNone : forall L1 L2 : list A, Olist L1 -> Olist L2 -> getMin L1 L2 = None -> forall a b : A, In a L1 -> In b L2 -> ~ test a b.
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. case (ltADec a a0); intros s; auto. Casec s; intros s; auto. intros H'1 a2 b H'2; Elimc H'2; intros H'2; [ rewrite <- H'2 | idtac ]; auto. intros H'3; red in |- *; intros H'4; absurd (In b (a0 :: l0)); auto. apply OlistUnique with (a := a); auto. intros H'3; apply (H' (a0 :: l0)); auto. apply OlistInv with (a := a); auto. generalize H'0; elim l0; auto. intros H'1 H'2 a2 b H'3 H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto. Elimc H'3; intros H'3; [ rewrite <- H'3 | idtac ]. red in |- *; intros H'5; absurd (eqA a0 a); auto. Contradict H'3; auto. apply OlistUnique with (a := a0); auto. apply OlistSkip with (b := a); auto. intros a2 l1 H'1 H'2. case (ltADec a a2); intros s1; auto. Casec s1; intros s1; auto. intros H'3 a3 b H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto. intros H'5; Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto. red in |- *; intros H'6; absurd (eqA a0 a); auto. Contradict H'5; auto. apply OlistUnique with (a := a); auto. apply OlistCons; auto. apply OlistInv with (a := a0); auto. intros H'5; Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]. Contradict H'4; auto. apply OlistUnique with (a := a0); auto. apply OlistSkip with (b := a); auto. apply (H' (a2 :: l1)); auto. apply OlistInv with (a := a); auto. apply OlistInv with (a := a0); auto. intros H'3 a3 b H'4 H'5. Elimc H'5; simpl in |- *; intros H'5; [ rewrite <- H'5 | idtac ]; auto. apply H'1; auto. apply OlistSkip with (b := a2); auto. Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto. Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]. red in |- *; intros H'6; absurd (eqA a2 a); auto. Contradict H'4. apply OlistUnique with (a := a2); auto. apply OlistSkip with (b := a); auto. apply H'1; auto. apply OlistSkip with (b := a2); auto. case (testDec a a2 s1); auto. intros H'3 H'4; discriminate. intros H'3 H'4 a3 b H'5 H'6. Elimc H'6; simpl in |- *; intros H'6; [ rewrite <- H'6 | idtac ]. Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]. red in |- *; intros H'7; absurd (eqA a0 a); auto. Contradict H'5. apply OlistUnique with (a := a0); auto. apply OlistSkip with (b := a); auto. Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]. Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto. Contradict H'5. apply OlistUnique with (a := a); auto. apply eqATrans with a2; auto. apply H'1; auto. apply OlistSkip with (b := a2); auto. case (testDec a a0 s); auto. intros H'1 H'2; discriminate. intros H'1 H'2 a2 b H'3; Elimc H'3; intros H'3; [ rewrite <- H'3 | idtac ]; auto. intros H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto. Contradict H'4; auto. apply OlistUnique with (a := a0); auto. apply eqATrans with a; auto. intros H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]. Contradict H'3; auto. apply OlistUnique with (a := a); auto. apply eqATrans with a0; auto. apply (H' l0); auto. apply OlistInv with (a := a); auto. apply OlistInv with (a := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)