proposition: Lemma sum_odd_3_bis : \sum_(0 <= i < 6 | odd i) i = 3^2.
proof: Proof. rewrite big_mkcond big_nat_recr //= -big_mkcond /=. Abort. Lemma prod_odd_3_bis : \big[muln/1]_(0 <= i < 6 | odd i) i = 3^2. Proof. rewrite big_mkcond big_nat_recr //= -big_mkcond /=. Abort. About bigD1. Lemma sum_odd_even_all n : \sum_(0 <= i < n) i = \sum_(0 <= i < n | odd i) i + \sum_(0 <= i < n | ~~ odd i) i. Proof. Search _ (~~ _) inside bigop. by rewrite (bigID odd). Qed.
imports: mathcomp(all_ssreflect)