proposition: Lemma BZsumC x y: x +z y = y +z x.
proof: Proof. rewrite /BZsum - lock /BZsum_v2. case:(p_or_not_p (inc x BZp)) => hx;case:(p_or_not_p (inc y BZp)) => hy. - by rewrite (Y_true (conj hx hy)) (Y_true (conj hy hx)) csumC. - have ha: ~(inc x BZp /\ inc y BZp) by case. have hb: ~(inc y BZp /\ inc x BZp) by case. have hc: ~(~ inc x BZp /\ ~ inc y BZp) by case. have hd: ~(~ inc y BZp /\ ~ inc x BZp) by case. have he:~(inc y BZp /\ ~ inc x BZp) by case. by Ytac0; Ytac0; Ytac0; Ytac0; Ytac0; rewrite (Y_true (conj hx hy)). - have ha: ~(inc x BZp /\ inc y BZp) by case. have hb: ~(inc y BZp /\ inc x BZp) by case. have hc: ~(~ inc x BZp /\ ~ inc y BZp) by case. have hd: ~(~ inc y BZp /\ ~ inc x BZp) by case. have he:~(inc x BZp /\ ~ inc y BZp) by case. by Ytac0; Ytac0; Ytac0; Ytac0; Ytac0; rewrite (Y_true (conj hy hx)). - have ha: ~(inc x BZp /\ inc y BZp) by case. have hb: ~(inc y BZp /\ inc x BZp) by case. by Ytac0;Ytac0; rewrite (Y_true (conj hx hy)) (Y_true (conj hy hx)) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)