proposition: Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat.
proof: Proof. simple induction n. - replace (2 * 0)%nat with 0%nat; [ apply le_n | ring ]. - intros; replace (2 * S n0)%nat with (S (S (2 * n0))). + apply le_n_S; apply le_S; assumption. + replace (S (S (2 * n0))) with (2 * n0 + 2)%nat; [ idtac | ring ]. replace (S n0) with (n0 + 1)%nat; [ idtac | ring ]. ring. Qed.
imports: Compare Rbase Rfunctions Rseries PartSum Binomial Lia