proposition: Theorem geMinIn : forall (L1 L2 : list A) (a : A), Olist L1 -> Olist L2 -> getMin L1 L2 = Some a -> In a L1.
proof: Proof. intros L1; elim L1; simpl in |- *. intros L2; case L2; simpl in |- *; auto with datatypes core. intros a H' H'0 H'1; discriminate. intros a l a0 H' H'0 H'1; discriminate. intros a l H' L2; case L2; simpl in |- *; auto with datatypes core. intros a0 H'0 H'1 H'2; discriminate. intros a0 l0 a1 H'0 H'1. case (ltADec a a0); intros s; auto. Casec s; intros s; auto. intros H'2; right. apply (H' (a0 :: l0)); 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; right. apply (H' (a2 :: l1)); auto. apply OlistInv with (a := a); auto. apply OlistInv with (a := a0); auto. intros H'4; case H'2; auto. apply OlistSkip with (b := a2); auto. case (testDec a a2 s1); auto. intros H'4 H'5; inversion H'5; auto. intros H'4 H'5; case H'2; auto. apply OlistSkip with (b := a2); auto. case (testDec a a0 s); auto. intros H'2 H'3; inversion H'3; auto. intros H'2 H'3; right. apply (H' l0); auto. apply OlistInv with (a := a); auto. apply OlistInv with (a := a0); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)