proposition: Lemma proper_0 : Proper (S.Equal ==> eq ==> eq) pick_variety.
proof: Proof. intros x1 y1 HXY1. intros x2 y2 HXY2. rewrite HXY2; clear HXY2; clear x2. unfold pick_variety; unfold pick_variety_aux. unfold STexists_. induction y2; try reflexivity. rewrite IHy2; clear IHy2. assert (HEqMem : forall e, S.mem e x1 = S.mem e y1) by (intro; apply SWP.Dec.F.mem_m; intuition); clear HXY1. assert (HF : forall n a, (fix F (n : nat) : cartesianPower positive (S (S n)) -> bool := match n as n0 return (cartesianPower positive (S (S n0)) -> bool) with | 0 => fun t0 : cartesianPower positive 2 => S.mem (fst t0) x1 && S.mem (snd t0) x1 | S n0 => fun t0 : cartesianPower positive (S (S (S n0))) => S.mem (headCP t0) x1 && F n0 (tailCP t0) end) n a = (fix F (n : nat) : cartesianPower positive (S (S n)) -> bool := match n as n0 return (cartesianPower positive (S (S n0)) -> bool) with | 0 => fun t0 : cartesianPower positive 2 => S.mem (fst t0) y1 && S.mem (snd t0) y1 | S n0 => fun t0 : cartesianPower positive (S (S (S n0))) => S.mem (headCP t0) y1 && F n0 (tailCP t0) end) n a) by (induction n; try (intro; do 2 (rewrite HEqMem); reflexivity); intro ; rewrite HEqMem; rewrite IHn; reflexivity). unfold pick_variety_auxCP. rewrite HF; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets