fact: Fixpoint bgcdn (k m n : nat) := if m == 0 then n else if m == 1 then 1 else if n == 0 then m else if n == 1 then 1 else if k is k1.+1 then if odd m then if odd n then let m1 := maxn m n in let n1 := minn m n in bgcdn k1 (m1 - n1)./2 n1 else bgcdn k1 m n./2 else if odd n then bgcdn k1 m./2 n else (bgcdn k1 m./2 n./2).*2 else 1.
imports: mathcomp(all_ssreflect)