proposition: Lemma gcd_partial_proof: forall x0 y0, (fun e => (VX e)=x0 /\ (VY e)=y0) |= gcd {= fun e => (Zis_gcd x0 y0 (VX e)) =}.
proof: Proof. intros x0 y0. apply PHL.soundness. simpl. intros e; intuition subst. constructor 1 with (x:=fun e'=> forall d, (Zis_gcd (VX e') (VY e') d) ->(Zis_gcd (VX e) (VY e) d)); simpl. intuition auto with zarith. replace (snd e') with (fst e') in H; auto with zarith. Qed.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia