[apply le_n.
|apply (bool_elim ? (p n1));intros
[rewrite > true_to_sigma_p_Sn
[rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
[apply le_plus
[apply le_n.
|apply (bool_elim ? (p n1));intros
[rewrite > true_to_sigma_p_Sn
[rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
[apply le_plus
[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
[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