(* --------------------------------------------------------------------
 * Copyright (c) - 2012--2016 - IMDEA Software Institute
 * Copyright (c) - 2012--2021 - Inria
 * Copyright (c) - 2012--2021 - Ecole Polytechnique
 *
 * Distributed under the terms of the CeCILL-B-V1 license
 * -------------------------------------------------------------------- *)

(* This API has been mostly inspired from the [bigop] library of the
 * ssreflect Coq extension. *)

pragma +implicits.

(* -------------------------------------------------------------------- *)
require import AllCore List Ring.
require (*--*) Monoid.

import Ring.IntID.

(* -------------------------------------------------------------------- *)
type t.

clone export Monoid as Support with type t <- t.
clear [Support.* Support.Axioms.*].

(* -------------------------------------------------------------------- *)
op big (P : 'a -> bool) (F : 'a -> t) (r : 'a list) =
  foldr Support.(+) idm (map F (filter P r)).

(* -------------------------------------------------------------------- *)
abbrev bigi (P : int -> bool) (F : int -> t) i j =
  big P F (range i j).

(* -------------------------------------------------------------------- *)
lemma big_nil (P : 'a -> bool) (F : 'a -> t): big P F [] = idm.
proof. by []. qed.

(* -------------------------------------------------------------------- *)
lemma big_cons (P : 'a -> bool) (F : 'a -> t) x s:
  big P F (x :: s) = if P x then F x + big P F s else big P F s.
proof. by rewrite {1}/big /= (@fun_if (map F)); case (P x). qed.

lemma big_consT (F : 'a -> t) x s:
  big predT F (x :: s) = F x + big predT F s.
proof. by apply/big_cons. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_rec (K : t -> bool) r P (F : 'a -> t):
  K idm => (forall i x, P i => K x => K (F i + x)) => K (big P F r).
proof.
  move=> K0 Kop; elim: r => //= i r; rewrite big_cons.
  by case (P i) => //=; apply/Kop.
qed.

lemma nosmt big_ind (K : t -> bool) r P (F : 'a -> t):
     (forall x y, K x => K y => K (x + y))
  => K idm => (forall i, P i => K (F i))
  => K (big P F r).
proof.
  move=> Kop Kidx K_F; apply/big_rec => //.
  by move=> i x Pi Kx; apply/Kop => //; apply/K_F.
qed.

lemma nosmt big_rec2:
  forall (K : t -> t -> bool) r P (F1 F2 : 'a -> t),
       K idm idm
    => (forall i y1 y2, P i => K y1 y2 => K (F1 i + y1) (F2 i + y2))
    => K (big P F1 r) (big P F2 r).
proof.
  move=> K r P F1 F2 KI KF; elim: r => //= i r IHr.
  by rewrite !big_cons; case (P i) => ? //=; apply/KF.
qed.

lemma nosmt big_ind2:
  forall (K : t -> t -> bool) r P (F1 F2 : 'a -> t),
       (forall x1 x2 y1 y2, K x1 x2 => K y1 y2 => K (x1 + y1) (x2 + y2))
    => K idm idm
    => (forall i, P i => K (F1 i) (F2 i))
    => K (big P F1 r) (big P F2 r).
proof.
  move=> K r P F1 F2 Kop KI KF; apply/big_rec2 => //.
  by move=> i x1 x2 Pi Kx1x2; apply/Kop => //; apply/KF.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_endo (f : t -> t):
     f idm = idm
  => (forall (x y : t), f (x + y) = f x + f y)
  => forall r P (F : 'a -> t),
       f (big P F r) = big P (f \o F) r.
proof.
  (* FIXME: should be a consequence of big_morph *)
  move=> fI fM; elim=> //= i r IHr P F; rewrite !big_cons.
  by case (P i) => //=; rewrite 1?fM IHr.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_map ['a 'b] (h : 'b -> 'a) (P : 'a -> bool) F s:
  big P F (map h s) = big (P \o h) (F \o h) s.
proof. by elim: s => // x s; rewrite map_cons !big_cons=> ->. qed.

lemma nosmt big_mapT ['a 'b] (h : 'b -> 'a) F s: (* -> big_map_predT *)
  big predT F (map h s) = big predT (F \o h) s.
proof. by rewrite big_map. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_comp ['a] (h : t -> t) (P : 'a -> bool) F s:
  h idm = idm => morphism_2 h Support.(+) Support.(+) =>
  h (big P F s) = big P (h \o F) s.
proof.
  move=> Hidm Hh;elim: s => // x s; rewrite !big_cons => <-.
  by rewrite /(\o) -Hh;case (P x) => //.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_nth x0 (P : 'a -> bool) (F : 'a -> t) s:
  big P F s = bigi (P \o (nth x0 s)) (F \o (nth x0 s)) 0 (size s).
proof. by rewrite -{1}(@mkseq_nth x0 s) /mkseq big_map. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_const (P : 'a -> bool) x s:
  big P (fun i => x) s = iter (count P s) ((+) x) idm.
proof.
  elim: s=> [|y s ih]; [by rewrite iter0 | rewrite big_cons /=].
  by rewrite ih; case (P y) => //; rewrite addzC iterS // count_ge0.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_seq1 (F : 'a -> t) x: big predT F [x] = F x.
proof. by rewrite big_cons big_nil addm0. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_mkcond (P : 'a -> bool) (F : 'a -> t) s:
  big P F s = big predT (fun i => if P i then F i else idm) s.
proof.
  elim: s=> // x s ih; rewrite !big_cons -ih /predT /=.
  by case (P x)=> //; rewrite add0m.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_filter (P : 'a -> bool) F s:
  big predT F (filter P s) = big P F s.
proof. by elim: s => //= x s; case (P x)=> //; rewrite !big_cons=> -> ->. qed.

(* -------------------------------------------------------------------- *)
lemma big_filter_cond (P1 P2 : 'a -> bool) F s:
  big P2 F (filter P1 s) = big (predI P1 P2) F s.
proof. by rewrite -big_filter -(@big_filter _ _ s) predIC filter_predI. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_bigl (P1 P2 : 'a -> bool) (F : 'a -> t) s:
     (forall i, P1 i <=> P2 i)
  => big P1 F s = big P2 F s.
proof. by move=> h; rewrite /big (eq_filter h). qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_bigr (P : 'a -> bool) (F1 F2 : 'a -> t) s:
     (forall i, P i => F1 i = F2 i)
  => big P F1 s = big P F2 s.
proof.                          (* FIXME: big_rec2 *)
  move=> eqF; elim: s=> // x s; rewrite !big_cons=> <-.
  by case (P x)=> // /eqF <-.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_distrl ['a] (op_ : t -> t -> t) (P : 'a -> bool) F s t:
     left_zero idm op_
  => left_distributive op_ Support.(+)
  => op_ (big P F s) t = big P (fun a => op_ (F a) t) s.
proof.
  move=> mulm1 mulmDl; pose G := fun x => op_ x t.
  move: (big_comp G P) => @/G /= -> //.
    by rewrite mulm1. by move=> t1 t2; rewrite mulmDl.
qed.

lemma nosmt big_distrr ['a] (op_ : t -> t -> t) (P : 'a -> bool) F s t:
      right_zero idm op_
   => right_distributive op_ Support.(+)
   => op_ t (big P F s) = big P (fun a => op_ t (F a)) s.
proof.
  move=> mul1m mulmDr; pose G := fun x => op_ t x.
  move: (big_comp G P) => @/G /= -> //.
    by rewrite mul1m. by move=> t1 t2; rewrite mulmDr.
qed.

lemma nosmt big_distr ['a 'b] (op_ : t -> t -> t)
  (P1 : 'a -> bool) (P2 : 'b -> bool) F1 s1 F2 s2 :
     commutative op_
  => left_zero idm op_
  => left_distributive op_ Support.(+)
  => op_ (big P1 F1 s1) (big P2 F2 s2) =
     big P1 (fun a1 => big P2 (fun a2 => op_ (F1 a1) (F2 a2)) s2) s1.
proof.
  move=> mulmC mulm1 mulmDl; rewrite big_distrl //.
  apply/eq_bigr=> i _ /=; rewrite big_distrr //.
    by move=> x; rewrite mulmC mulm1.
  by move=> x y z; rewrite !(mulmC x) mulmDl.
qed.

(* -------------------------------------------------------------------- *)
lemma big_andbC (P Q : 'a -> bool) F s:
  big (fun x => P x /\ Q x) F s = big (fun x => Q x /\ P x) F s.
proof. by apply/eq_bigl=> i. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_big (P1 P2 : 'a -> bool) (F1 F2 : 'a -> t) s:
     (forall i, P1 i <=> P2 i)
  => (forall i, P1 i => F1 i = F2 i)
  => big P1 F1 s = big P2 F2 s.
proof. by move=> /eq_bigl <- /eq_bigr <-. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt congr_big r1 r2 P1 P2 (F1 F2 : 'a -> t):
     r1 = r2
  => (forall x, P1 x <=> P2 x)
  => (forall i, P1 i => F1 i = F2 i)
  => big P1 F1 r1 = big P2 F2 r2.
proof. by move=> <-; apply/eq_big. qed.

(* -------------------------------------------------------------------- *)
lemma big_hasC (P : 'a -> bool) (F : 'a -> t) s: !has P s =>
  big P F s = idm.
proof.
  rewrite -big_filter has_count -size_filter.
  by rewrite ltz_def size_ge0 /= => /size_eq0 ->.
qed.

(* -------------------------------------------------------------------- *)
lemma big_pred0_eq (F : 'a -> t) s: big pred0 F s = idm.
proof. by rewrite big_hasC // has_pred0. qed.

(* -------------------------------------------------------------------- *)
lemma big_pred0 (P : 'a -> bool) (F : 'a -> t) s:
  (forall i, P i <=> false) => big P F s = idm.
proof. by move=> h; rewrite -(@big_pred0_eq F s); apply/eq_bigl. qed.

(* -------------------------------------------------------------------- *)
lemma big_cat (P : 'a -> bool) (F : 'a -> t) s1 s2:
  big P F (s1 ++ s2) = big P F s1 + big P F s2.
proof.
  rewrite !(@big_mkcond P); elim: s1 => /= [|i s1 ih].
    by rewrite (@big_nil P F) add0m.
  by rewrite !big_cons /(predT i) /= ih addmA.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_catl (P : 'a -> bool) (F : 'a -> t) s1 s2: !has P s2 =>
  big P F (s1 ++ s2) = big P F s1.
proof. by rewrite big_cat => /big_hasC ->; rewrite addm0. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_catr (P : 'a -> bool) (F : 'a -> t) s1 s2: !has P s1 =>
  big P F (s1 ++ s2) = big P F s2.
proof. by rewrite big_cat => /big_hasC ->; rewrite add0m. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_rcons (P : 'a -> bool) (F : 'a -> t) s x:
  big P F (rcons s x) = if P x then big P F s + F x else big P F s.
proof.
  by rewrite -cats1 big_cat big_cons big_nil; case: (P x); rewrite !addm0.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_big_perm (P : 'a -> bool) (F : 'a -> t) s1 s2:
  perm_eq s1 s2 => big P F s1 = big P F s2.
proof.
  move=> /perm_eqP; rewrite !(@big_mkcond P).
  elim s1 s2 => [|i s1 ih1] s2 eq_s12.
    by case s2 eq_s12 => // i s2 h; have := h (pred1 i); smt.
  have r2i: mem s2 i by rewrite -has_pred1 has_count -eq_s12 #smt.
  have/splitPr [s3 s4] ->> := r2i.
  rewrite big_cat !big_cons /(predT i) /=.
  rewrite addmCA; congr; rewrite -big_cat; apply/ih1=> a.
  by have := eq_s12 a; rewrite !count_cat /= addzCA => /addzI.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_big_perm_map (F : 'a -> t) s1 s2:
  perm_eq (map F s1) (map F s2) => big predT F s1 = big predT F s2.
proof.
by move=> peq; rewrite -!(@big_map F predT idfun) &(eq_big_perm).
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_seq_cond (P : 'a -> bool) (F : 'a -> t) s:
  big P F s = big (fun i => mem s i /\ P i) F s.
proof. by rewrite -!(@big_filter _ _ s); congr; apply/eq_in_filter. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_seq (F : 'a -> t) s:
  big predT F s = big (fun i => mem s i) F s.
proof. by rewrite big_seq_cond; apply/eq_bigl. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_rem (P : 'a -> bool) (F : 'a -> t) s x: mem s x =>
  big P F s = (if P x then F x else idm) + big P F (rem x s).
proof.
  by move/perm_to_rem/eq_big_perm=> ->; rewrite !(@big_mkcond P) big_cons.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt bigD1 (F : 'a -> t) s x: mem s x => uniq s =>
  big predT F s = F x + big (predC1 x) F s.
proof. by move=> /big_rem-> /rem_filter->; rewrite big_filter. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt bigD1_cond P (F : 'a -> t) s x: P x => mem s x => uniq s =>
  big P F s = F x + big (predI P (predC1 x)) F s.
proof.
move=> Px sx uqs; rewrite -big_filter (@bigD1 _ _ x) ?big_filter_cond //.
  by rewrite mem_filter Px. by rewrite filter_uniq.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt bigD1_cond_if P (F : 'a -> t) s x: uniq s => big P F s =
  (if mem s x /\ P x then F x else idm) + big (predI P (predC1 x)) F s.
proof.
case: (mem s x /\ P x) => [[Px sx]|Nsx]; rewrite ?add0m /=.
  by apply/bigD1_cond.
move=> uqs; rewrite big_seq_cond eq_sym big_seq_cond; apply/eq_bigl=> i /=.
by case: (i = x) => @/predC1 @/predI [->>|].
qed.

(* -------------------------------------------------------------------- *)
lemma big_split (P : 'a -> bool) (F1 F2 : 'a -> t) s:
  big P (fun i => F1 i + F2 i) s = big P F1 s + big P F2 s.
proof.
  elim: s=> /= [|x s ih]; 1: by rewrite !big_nil addm0.
  rewrite !big_cons ih; case: (P x) => // _.
  by rewrite addmCA -!addmA addmCA.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt bigID (P : 'a -> bool) (F : 'a -> t) (a : 'a -> bool) s:
  big P F s = big (predI P a) F s + big (predI P (predC a)) F s.
proof.
  rewrite !(@big_mkcond _ F) -big_split /(/\) /[!].
  apply/eq_bigr => i _ /=.
  by rewrite /predI /predC; case: (a i); rewrite ?addm0 ?add0m.
qed.

(* -------------------------------------------------------------------- *)
lemma bigU ['a] (P Q : 'a -> bool) F s : (forall x, !(P x /\ Q x)) =>
  big (predU P Q) F s = big P F s + big Q F s.
proof.
move=> dj_PQ; rewrite (@bigID (predU _ _) _ P).
by congr; apply: eq_bigl => /#.
qed.

(* -------------------------------------------------------------------- *)
lemma bigEM ['a] (P : 'a -> bool) (F : 'a -> t) s :
  big predT F s = big P F s + big (predC P) F s.
proof. by rewrite -bigU 1:/#; apply: eq_bigl => /#. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_reindex ['a 'b]
  (P : 'a -> bool) (F : 'a -> t) (f : 'b -> 'a) (f' : 'a -> 'b) s
:
  cancel f' f => big P F s = big (P \o f) (F \o f) (map f' s).
proof. by move=> bij_ff'; rewrite -big_map -map_comp id_map. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_pair_pswap ['a 'b] p f s :
    big<:'a * 'b> p f s
  = big<:'b * 'a> (p \o pswap) (f \o pswap) (map pswap s).
proof. by apply/big_reindex; case. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_big_seq (F1 F2 : 'a -> t) s:
     (forall x, mem s x => F1 x = F2 x)
  => big predT F1 s = big predT F2 s.
proof. by move=> eqF; rewrite !big_seq; apply/eq_bigr. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt congr_big_seq (P1 P2: 'a -> bool) (F1 F2 : 'a -> t) s:
     (forall x, mem s x => P1 x = P2 x) =>
     (forall x, mem s x => P1 x => P2 x => F1 x = F2 x)
  => big P1 F1 s = big P2 F2 s.
proof.
  move=> eqP eqH; rewrite big_mkcond eq_sym big_mkcond eq_sym.
  apply/eq_big_seq=> x x_in_s /=; rewrite eqP //.
  by case (P2 x)=> // P2x; rewrite eqH // eqP.
qed.

(* -------------------------------------------------------------------- *)
lemma big1_eq (P : 'a -> bool) s: big P (fun x => idm) s = idm.
proof.
  rewrite big_const; elim/natind: (count _ _)=> n.
    by move/iter0<:t> => ->.
  by move/iterS<:t> => -> ->; rewrite addm0.
qed.

(* -------------------------------------------------------------------- *)
lemma big1 (P : 'a -> bool) F s:
  (forall i, P i => F i = idm) => big P F s = idm.
proof. by move/eq_bigr=> ->; apply/big1_eq. qed.

(* -------------------------------------------------------------------- *)
lemma big1_seq (P : 'a -> bool) F s:
  (forall i, P i /\ (mem s i) => F i = idm) => big P F s = idm.
proof. by move=> eqF1; rewrite big_seq_cond big_andbC big1. qed.

(* -------------------------------------------------------------------- *)
lemma big_eq_idm_filter ['a] (P : 'a -> bool) (F : 'a -> t) s :
  (forall (x : 'a), !P x => F x = idm) => big predT F s = big P F s.
proof.
by move=> eq1; rewrite (@bigEM P) (@big1 (predC _)) // addm0.
qed.

(* -------------------------------------------------------------------- *)
lemma big_flatten (P : 'a -> bool) F rr :
  big P F (flatten rr) = big predT (fun s => big P F s) rr.
proof.
elim: rr => /= [|r rr ih]; first by rewrite !big_nil.
by rewrite flatten_cons big_cat big_cons -ih.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_pair ['a 'b] F (s : ('a * 'b) list) : uniq s =>
  big predT F s =
    big predT (fun a =>
        big predT F (filter (fun xy : _ * _ => xy.`1 = a) s))
      (undup (map fst s)).
proof.
move=> /perm_eq_pair /eq_big_perm /(_ predT F) ->.
by rewrite big_flatten big_map.
qed.

(* -------------------------------------------------------------------- *)
lemma big_nseq_cond (P : 'a -> bool) F n x :
  big P F (nseq n x) = if P x then iter n ((+) (F x)) idm else idm.
proof.
elim/natind: n => [n le0_n|n ge0_n ih]; first by rewrite ?(nseq0_le, iter0).
by rewrite nseqS // big_cons ih; case: (P x) => //; rewrite iterS.
qed.

(* -------------------------------------------------------------------- *)
lemma big_nseq (F : 'a -> t) n x :
  big predT F (nseq n x) = iter n ((+) (F x)) idm.
proof. by apply/big_nseq_cond. qed.

(* -------------------------------------------------------------------- *)
lemma big_undup ['a] (P : 'a -> bool) F s :
  big P F s = big P (fun a => iter (count (pred1 a) s) ((+) (F a)) idm) (undup s).
proof.
have <- := eq_big_perm P F _ _ (perm_undup_count s).
rewrite big_flatten big_map (@big_mkcond P); apply/eq_big => //=.
by move=> @/(\o) /= x _; apply/big_nseq_cond.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt exchange_big (P1 : 'a -> bool) (P2 : 'b -> bool) F s1 s2:
   big P1 (fun a => big P2 (F a) s2) s1 =
   big P2 (fun b => big P1 (fun a => F a b) s1) s2.
proof.
  elim: s1 s2 => [|a s1 ih] s2; first by rewrite big_nil big1_eq.
  rewrite big_cons ih; case: (P1 a)=> h; rewrite -?big_split;
    by apply/eq_bigr=> x _ /=; rewrite big_cons h.
qed.

(* -------------------------------------------------------------------- *)
lemma partition_big ['a 'b] (px : 'a -> 'b) P Q (F : 'a -> t) s s' :
     uniq s'
  => (forall x, mem s x => P x => mem s' (px x) /\ Q (px x))
  => big P F s = big Q (fun x => big (fun y => P y /\ px y = x) F s) s'.
proof.
move=> uq_s'; elim: s => /~= [|x xs ih] hm.
  by rewrite big_nil big1_eq.
rewrite big_cons; case: (P x) => /= [Px|PxN]; last first.
  rewrite ih //; 1: by move=> y y_xs; apply/hm; rewrite y_xs.
  by apply/eq_bigr=> i _ /=; rewrite big_cons /= PxN.
have := hm x; rewrite Px /= => -[s'_px Qpx]; apply/eq_sym.
rewrite (@bigD1_cond _ _ _ (px x)) //= big_cons /= Px /=.
rewrite -addmA; congr; apply/eq_sym; rewrite ih.
  by move=> y y_xs; apply/hm; rewrite y_xs.
rewrite (@bigD1_cond _ _ _ (px x)) //=; congr.
apply/eq_bigr=> /= i [Qi @/predC1]; rewrite eq_sym => ne_pxi.
by rewrite big_cons /= ne_pxi.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_allpairs f F s t:
    big predT F (allpairs<:'a, 'b, 'c> f s t)
  = big predT (fun x => big predT (fun y => F (f x y)) t) s.
proof.
elim: s t => [|x s ih] t //=. 
by rewrite allpairs_consl big_cat ih big_consT big_map.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int_cond m n P F:
  bigi P F m n = bigi (fun i => m <= i < n /\ P i) F m n.
proof. by rewrite big_seq_cond; apply/eq_bigl=> i /=; smt. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int m n F:
  bigi predT F m n = bigi (fun i => m <= i < n) F m n.
proof. by rewrite big_int_cond. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt congr_big_int (m1 n1 m2 n2 : int) P1 P2 F1 F2:
       m1 = m2 => n1 = n2
    => (forall i, m1 <= i < n2 => P1 i = P2 i)
    => (forall i, P1 i /\ (m1 <= i < n2) => F1 i = F2 i)
    => bigi P1 F1 m1 n1 = bigi P2 F2 m2 n2.
proof.
  move=> <- <- eqP12 eqF12; rewrite big_seq_cond (@big_seq_cond P2).
  by apply/eq_big=> i /=; rewrite mem_range #smt.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt eq_big_int (m n : int) F1 F2:
     (forall i, m <= i < n => F1 i = F2 i)
  => bigi predT F1 m n = bigi predT F2 m n.
proof. by move=> eqF; apply/congr_big_int. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_ltn_cond (m n : int) P F: m < n =>
  let x = bigi P F (m+1) n in
  bigi P F m n = if P m then F m + x else x.
proof. by move/range_ltn=> ->; rewrite big_cons. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_ltn (m n : int) F: m < n =>
  bigi predT F m n = F m + bigi predT F (m+1) n.
proof. by move/big_ltn_cond=> /= ->. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_geq (m n : int) P F: n <= m =>
  bigi P F m n = idm.
proof. by move/range_geq=> ->; rewrite big_nil. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_addn (m n a : int) P F:
    bigi P F (m+a) n
  = bigi (fun i => P (i+a)) (fun i => F (i+a)) m (n-a).
proof.
rewrite range_addl big_map; apply/eq_big.
  by move=> i /=; rewrite /(\o) addzC.
by move=> i /= _; rewrite /(\o) addzC.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int1 n F: bigi predT F n (n+1) = F n.
proof. by rewrite big_ltn 1:/# big_geq // addm0. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_cat_int (n m p : int) P F: m <= n => n <= p =>
  bigi P F m p = (bigi P F m n) + (bigi P F n p).
proof. by move=> lemn lenp; rewrite -big_cat -range_cat. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int_recl (n m : int) F: m <= n =>
  bigi predT F m (n+1) = F m + bigi predT (fun i => F (i+1)) m n.
proof. by move=> lemn; rewrite big_ltn 1?big_addn /= 1:/#. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int_recr (n m : int) F: m <= n =>
  bigi predT F m (n+1) = bigi predT F m n + F n.
proof. by move=> lemn; rewrite (@big_cat_int n) ?big_int1 //#. qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int_recl_cond (n m : int) P F: m <= n =>
  bigi P F m (n+1) =
    (if P m then F m else idm) +
      bigi (fun i => P (i+1)) (fun i => F (i+1)) m n.
proof.
by move=> lemn; rewrite big_mkcond big_int_recl //= -big_mkcond.
qed.

(* -------------------------------------------------------------------- *)
lemma nosmt big_int_recr_cond (n m : int) P F: m <= n =>
  bigi P F m (n+1) =
    bigi P F m n + (if P n then F n else idm).
proof. by move=> lemn; rewrite !(@big_mkcond P) big_int_recr. qed.