proposition: Lemma proper_3 : Proper (SP.Equal ==> SSP.Equal ==> eqopp) pick_lengths_aux.
proof: Proof. intros x1 y1 HXY1. intros x2 y2 HXY2. unfold pick_lengths_aux. assert (H : eqop (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter x1 s2))) x2) (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter y1 s2))) y2)). apply proper_2. apply proper_1. intro; apply proper_0. apply SPWP.inter_equal_1; assumption. assumption. case_eq (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter y1 s2))) y2); case_eq (exists_witness (fun s2 : SSP.elt => negb (SP.is_empty (SP.inter x1 s2))) x2). simpl; intuition. intros HCN e HCS. simpl. rewrite HCS in H; rewrite HCN in H. simpl in H. assumption. intros e HCS HCN. simpl. rewrite HCS in H; rewrite HCN in H. simpl in H. assumption. intuition. Qed.
imports: Recdef NArith GeoCoq.Utils.sets