proposition: Lemma BZgcd_C a b: BZgcd a b = BZgcd b a.
proof: Proof. suff: BZ_ideal2 a b = BZ_ideal2 b a by rewrite /BZgcd => ->. by set_extens t => /Zo_P [pa [u [v [uc vz etc]]]]; apply:Zo_i => //; exists v ;exists u; rewrite BZsumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)