proposition: Lemma pick_lines_ok_1 : forall s1 s2 ss sp, pick_lines ss sp = Some(s1,s2) -> SS.In s1 ss.
proof: Proof. intros s1 s2 ss sp H. unfold pick_lines in H. case_eq (exists_witness (fun s : SS.elt => match pick_lines_aux s (SS.remove s ss) sp with | Some _ => true | None => false end) ss). intros e1 HEW1. rewrite HEW1 in H. unfold pick_lines_aux in H. case_eq (exists_witness (fun s2 : SS.elt => pick_line (S.inter e1 s2) sp) (SS.remove e1 ss)). intros e2 HEW2. rewrite HEW2 in H. assert (HEq1 : e1 = s1) by (injection H; intros; assumption). rewrite HEq1 in *. assert (HEq2 : e2 = s2) by (injection H; intros; assumption). rewrite HEq2 in *. apply exists_witness_ok with (fun s : SS.elt => match pick_lines_aux s (SS.remove s ss) sp with | Some _ => true | None => false end). intros x y HXY. assert (SS.Equal (SS.remove x ss) (SS.remove y ss)) by (apply SSWP.Dec.F.remove_m; try assumption; reflexivity). assert (eqopp (pick_lines_aux x (SS.remove x ss) sp) (pick_lines_aux y (SS.remove y ss) sp)). apply proper_3; auto. case_eq (pick_lines_aux x (SS.remove x ss) sp); intros; case_eq (pick_lines_aux y (SS.remove y ss) sp); intros. reflexivity. rewrite H2 in H1; rewrite H3 in H1. unfold eqop in H1; simpl in H1. intuition. rewrite H2 in H1; rewrite H3 in H1. unfold eqop in H1; simpl in H1. intuition. reflexivity. assumption. intro HEW2. rewrite HEW2 in H. discriminate. intro HEW. rewrite HEW in H. discriminate. Qed.
imports: Recdef NArith GeoCoq.Utils.sets