proposition: Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat), (forall i, f1 i >= f2 i) -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
proof: Proof. intros. funelim (rifoldr plus 0 f1). - constructor. - apply Nat.add_le_mono. + apply H0. + apply H. intros. apply H0. Qed.
imports: Arith List Program Equations.Prop.Equations