proposition: Lemma gcd_total_proof: forall x0 y0, (fun e => (VX e)=x0 /\ (VY e)=y0 /\ x0 > 0 /\ y0 > 0) |= gcd [= fun e => (Zis_gcd x0 y0 (VX e)) =].
proof: Proof. intros x0 y0. apply THL.soundness. simpl. intros e; intuition subst. constructor 1 with (x:=fun e' => (VX e') > 0 /\ (VY e') > 0 /\ forall d, (Zis_gcd (VX e') (VY e') d) ->(Zis_gcd (VX e) (VY e) d)); simpl. constructor 1 with (x:=fun e1 e0 => Zwf 0 ((VX e1)+(VY e1)) ((VX e0)+(VY e0))). constructor 1. apply wf_inverse_image with (f:=fun e=>(VX e)+(VY e)). auto with datatypes. unfold Zwf; simpl; (intuition auto with zarith). replace (snd e') with (fst e') in H5; auto with zarith. cut ((fst e')<=(snd e')); auto with zarith. cut ((fst e')<>(snd e')); auto with zarith. Qed.
imports: ZArith Znumtheory hoarelogic Zwf Wellfounded Lia