proposition: Lemma pick_varieties_ok_1 : forall s1 s2 ss st, pick_varieties ss st = Some(s1,s2) -> SS.In s1 ss.
proof: Proof. intros s1 s2 ss st H. unfold pick_varieties in H. case_eq (exists_witness (fun s : SS.elt => match pick_varieties_aux s (SS.remove s ss) st with | Some _ => true | None => false end) ss). intros e1 HEW1. rewrite HEW1 in H. unfold pick_varieties_aux in H. case_eq (exists_witness (fun s2 : SS.elt => pick_variety (S.inter e1 s2) st) (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_varieties_aux s (SS.remove s ss) st 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_varieties_aux x (SS.remove x ss) st) (pick_varieties_aux y (SS.remove y ss) st)) by (apply proper_3; auto). case_eq (pick_varieties_aux x (SS.remove x ss) st); intros; case_eq (pick_varieties_aux y (SS.remove y ss) st); 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 Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets