proposition: Lemma fusc_coprime n: natp n -> BZcoprime (fuscz n) (fuscz (csucc n)).
proof: Proof. move:fusc_pr => [Ha Hb Hc Hd]; move: n; rewrite /fuscz. apply: fusc_induction. + rewrite Ha succ_zero Hb;apply:(BZ_coprime1r ZS0). + rewrite Hb; apply: BZ_coprime1l;apply:BZ_of_nat_i; apply:NS_fusc; fprops. + move => n nN. move:(NS_fusc nN) (NS_fusc (NS_succ nN)) => ha hb. move: (BZ_of_nat_i ha) (BZ_of_nat_i hb) => ha' hb'. rewrite (Hc _ nN) (Hd _ nN) - (BZsum_cN ha hb). by apply:(BZcoprime_add ha' hb'). + move => n nN sa _. rewrite - (double_succ nN). move: (NS_fusc nN)(NS_fusc (NS_succ nN)) => ha hb. move: (BZ_of_nat_i ha) (BZ_of_nat_i hb) => ha' hb'. rewrite (Hd _ nN) (Hc _ (NS_succ nN)) - (BZsum_cN ha hb). apply:BZcoprime_sym; rewrite BZsumC; apply: (BZcoprime_add hb' ha'). by apply:BZcoprime_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)