proposition: Lemma pick_lengths_ok_1 : forall s1 s2 ss, pick_lengths ss = Some(s1,s2) -> SSP.In s1 ss.
proof: Proof. intros s1 s2 ss H. unfold pick_lengths in H. case_eq (exists_witness (fun s : SSP.elt => match pick_lengths_aux s (SSP.remove s ss) with | Some _ => true | None => false end) ss). intros e1 HEW1. rewrite HEW1 in H. unfold pick_lengths_aux in H. case_eq (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter e1 s2))) (SSP.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 *. eapply exists_witness_ok; [|exact HEW1]. intros x y HXY. assert (SSP.Equal (SSP.remove x ss) (SSP.remove y ss)) by (apply SSPWP.Dec.F.remove_m; try assumption; reflexivity). assert (eqopp (pick_lengths_aux x (SSP.remove x ss)) (pick_lengths_aux y (SSP.remove y ss))). apply proper_3; auto. case_eq (pick_lengths_aux x (SSP.remove x ss)); intros; case_eq (pick_lengths_aux y (SSP.remove y ss)); intros. reflexivity. rewrite H2 in H1; rewrite H3 in H1. unfold eqop in H1; simpl in H1. contradiction. rewrite H2 in H1; rewrite H3 in H1. unfold eqop in H1; simpl in H1. contradiction. reflexivity. intro HEW2. rewrite HEW2 in H. discriminate H. intro HEW. rewrite HEW in H. discriminate H. Qed.
imports: Recdef NArith GeoCoq.Utils.sets