proposition: Lemma gcdn_greatest : forall n a b, (size_nat a + size_nat b <= n)%nat -> forall p, (p|a) -> (p|b) -> (p|gcdn n a b).
proof: Proof. intro n; induction n as [|n IHn]; intros a b. - destruct a, b; simpl; inversion 1. - destruct a as [a|a|], b as [b|b|]; simpl; try case compare_spec; simpl; auto. + intros LT LE p Hp1 Hp2. apply IHn; clear IHn; trivial. * apply le_S_n in LE. eapply Nat.le_trans; [|eapply LE]. rewrite Nat.add_comm, <- plus_n_Sm, <- plus_Sn_m. apply Nat.add_le_mono; trivial. apply size_nat_monotone, sub_decr, LT. * apply divide_xO_xI with a; trivial. apply (divide_add_cancel_l p _ a~1); trivial. now rewrite <- sub_xI_xI, sub_add. + intros LT LE p Hp1 Hp2. apply IHn; clear IHn; trivial. * apply le_S_n in LE. eapply Nat.le_trans; [|eapply LE]. apply Nat.add_le_mono; trivial. apply size_nat_monotone, sub_decr, LT. * apply divide_xO_xI with b; trivial. apply (divide_add_cancel_l p _ b~1); trivial. now rewrite <- sub_xI_xI, sub_add. + intros LE p Hp1 Hp2. apply IHn; clear IHn; trivial. * apply le_S_n in LE. simpl. now rewrite plus_n_Sm. * apply divide_xO_xI with a; trivial. + intros LE p Hp1 Hp2. apply IHn; clear IHn; trivial. * simpl. now apply le_S_n. * apply divide_xO_xI with b; trivial. + intros LE p Hp1 Hp2. destruct p as [p|p|]. * { change (gcdn n a b)~0 with (2*(gcdn n a b)). apply divide_mul_r. apply IHn; clear IHn. - apply le_S_n in LE. rewrite <- plus_n_Sm in LE. now apply Nat.lt_le_incl. - apply divide_xO_xI with p; trivial. now exists 1. - apply divide_xO_xI with p; trivial. now exists 1. } * { apply divide_xO_xO. apply IHn; clear IHn. - apply le_S_n in LE. rewrite <- plus_n_Sm in LE. now apply Nat.lt_le_incl. - now apply divide_xO_xO. - now apply divide_xO_xO. } * exists (gcdn n a b)~0. now rewrite mul_1_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef