proposition: Lemma BZsum_alt x y: intp x -> intp y -> BZsum_v2 x y = BZsum_v1 x y.
proof: Proof. have Hb := CS_sum2 (P x) (P y). rewrite /BZsum_v1 /BZsum_v2 pr1_pair pr2_pair => xz yz. move: (BZ_valN xz) (BZ_valN yz) => pxn pyn. case: (p_or_not_p (inc x BZp));case: (p_or_not_p (inc y BZp)) => hx hy. - have hxy: (inc x BZp /\ inc y BZp) by []. have sp: \0c <=c (P x +c P y) by apply: cle0x. Ytac0; Ytac0; Ytac0; rewrite !pr1_pair !pr2_pair (csum0l CS0); Ytac0. by rewrite (csubn0 Hb). - have hxy: ~ (inc x BZp /\ inc y BZp) by case. have hxy2: ~(~ inc x BZp /\ ~ inc y BZp) by case. have hxy3: (inc x BZp /\ ~ inc y BZp) by split. Ytac0; Ytac0; Ytac0; Ytac0; Ytac0; rewrite !pr1_pair !pr2_pair. by rewrite (Nsum0l pyn) (Nsum0r pxn). - have hxy: ~ (inc x BZp /\ inc y BZp) by case. have hxy2: ~(~ inc x BZp /\ ~ inc y BZp) by case. have hxy3: ~(inc x BZp /\ ~ inc y BZp) by case. Ytac0; Ytac0; Ytac0; Ytac0; rewrite !pr1_pair !pr2_pair. by Ytac0; rewrite pr1_pair pr2_pair (Nsum0l pyn) (Nsum0r pxn). - have hxy: ~(inc x BZp /\ inc y BZp) by case. have hxy2: (~ inc x BZp /\ ~ inc y BZp) by split. Ytac0; Ytac0; Ytac0; Ytac0; rewrite !pr1_pair !pr2_pair (csum0l CS0). by rewrite (BZsum_spec Hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)