proposition: Lemma remove_Inf : forall (m:farray)(Hm : Sort m)(x x':key)(e':elt), Inf (x',e') m -> Inf (x',e') (remove x m).
proof: Proof. induction m. simpl; intuition. intros. destruct a as (x'',e''). inversion_clear H. compute in H0. simpl; case (compare x x''); intuition. inversion_clear Hm. apply Inf_lt with (x'',e''); auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance