+(* a slightly more general result *)
+theorem le_sigma_p1:
+\forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat.
+(\forall i. i < n \to
+bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to
+sigma_p n p1 g1 \le sigma_p n p2 g2.
+intros.
+generalize in match H.
+elim n
+ [apply le_n.
+ |apply (bool_elim ? (p1 n1));intros
+ [apply (bool_elim ? (p2 n1));intros
+ [rewrite > true_to_sigma_p_Sn
+ [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
+ [apply le_plus
+ [lapply (H2 n1) as H5
+ [rewrite > H3 in H5.
+ rewrite > H4 in H5.
+ simplify in H5.
+ rewrite < plus_n_O in H5.
+ rewrite < plus_n_O in H5.
+ assumption
+ |apply le_S_S.apply le_n
+ ]
+ |apply H1.intros.
+ apply H2.apply le_S.assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |rewrite > true_to_sigma_p_Sn
+ [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
+ [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2).
+ apply le_plus
+ [lapply (H2 n1) as H5
+ [rewrite > H3 in H5.
+ rewrite > H4 in H5.
+ simplify in H5.
+ rewrite < plus_n_O in H5.
+ assumption
+ |apply le_S_S.apply le_n
+ ]
+ |apply H1.intros.
+ apply H2.apply le_S.assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ |apply (bool_elim ? (p2 n1));intros
+ [rewrite > false_to_sigma_p_Sn
+ [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
+ [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1).
+ apply le_plus
+ [lapply (H2 n1) as H5
+ [rewrite > H3 in H5.
+ rewrite > H4 in H5.
+ simplify in H5.
+ rewrite < plus_n_O in H5.
+ assumption
+ |apply le_S_S.apply le_n
+ ]
+ |apply H1.intros.
+ apply H2.apply le_S.assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |rewrite > false_to_sigma_p_Sn
+ [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
+ [apply H1.intros.
+ apply H2.apply le_S.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem lt_sigma_p:
+\forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
+(\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
+(\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to
+sigma_p n p g1 < sigma_p n p g2.
+intros 4.
+elim n
+ [elim H1.clear H1.
+ elim H2.clear H2.
+ elim H1.clear H1.
+ apply False_ind.
+ apply (lt_to_not_le ? ? H2).
+ apply le_O_n
+ |apply (bool_elim ? (p n1));intros
+ [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros
+ [rewrite > true_to_sigma_p_Sn
+ [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
+ [change with
+ (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2).
+ apply le_plus
+ [apply leb_true_to_le.assumption
+ |apply le_sigma_p.intros.
+ apply H1
+ [apply lt_to_le.apply le_S_S.assumption
+ |assumption
+ ]
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |rewrite > true_to_sigma_p_Sn
+ [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
+ [unfold lt.
+ rewrite > plus_n_Sm.
+ apply le_plus
+ [apply H1
+ [apply le_n
+ |assumption
+ ]
+ |apply H
+ [intros.apply H1
+ [apply lt_to_le.apply le_S_S.assumption
+ |assumption
+ ]
+ |elim H2.clear H2.
+ elim H5.clear H5.
+ elim H2.clear H2.
+ apply (ex_intro ? ? a).
+ split
+ [split
+ [elim (le_to_or_lt_eq a n1)
+ [assumption
+ |absurd (g1 a < g2 a)
+ [assumption
+ |apply leb_false_to_not_le.
+ rewrite > H2.
+ assumption
+ ]
+ |apply le_S_S_to_le.
+ assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ |rewrite > false_to_sigma_p_Sn
+ [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
+ [apply H
+ [intros.apply H1
+ [apply lt_to_le.apply le_S_S.assumption
+ |assumption
+ ]
+ |elim H2.clear H2.
+ elim H4.clear H4.
+ elim H2.clear H2.
+ apply (ex_intro ? ? a).
+ split
+ [split
+ [elim (le_to_or_lt_eq a n1)
+ [assumption
+ |apply False_ind.
+ apply not_eq_true_false.
+ rewrite < H6.
+ rewrite < H3.
+ rewrite < H2.
+ reflexivity
+ |apply le_S_S_to_le.
+ assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+ ]
+qed.
+