proposition: Lemma big_ord_recl : forall n F, \big[op/idx]_(i < n.+1) F i === op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)).
proof: Proof. move=> n F; pose G i := F (inord i). have eqFG: forall i, R (F i) (G i) by move=> i; rewrite /G inord_val;reflexivity. transitivity (\big[op/idx]_(i < n.+1) G i); first by apply eq_bigr=> *; apply eqFG. rewrite <- (big_mkord (S n) (fun _ => true) G), eqFG. rewrite -> big_ltn=> //; rewrite -> big_add1=> /=; rewrite -> big_mkord. apply H0; try reflexivity. by apply: eq_bigr => i _; rewrite -> eqFG; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops