proposition: Lemma pick_varieties_ok_2 : forall s1 s2 ss st, pick_varieties ss st = Some(s1,s2) -> SS.In s2 (SS.remove 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 s2 : SS.elt => pick_variety (S.inter s1 s2) st). intros x y HXY. apply proper_1; assumption. 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