proposition: Lemma sumToN2 b a : a <= b -> sumToN a <= sumToN b.
proof: Proof. revert a; induction b as [| b Hrecb]; intros. - simpl in |- *; rewrite (Nat.le_0_r a) in H; now subst. - rewrite Nat.lt_eq_cases in H; destruct H as [H | H]. + transitivity (sumToN b). * apply Hrecb; auto. apply Compat815.lt_n_Sm_le; auto. * cbn in |- *; apply le_S; rewrite Nat.add_comm. apply le_add_r. + subst a; reflexivity. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)