[apply le_n.
|apply (bool_elim ? (p n1));intros
[rewrite > true_to_pi_p_Sn
[rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
[apply le_times
[apply le_n.
|apply (bool_elim ? (p n1));intros
[rewrite > true_to_pi_p_Sn
[rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
[apply le_times