proposition: Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b.
proof: Proof. assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b). - intros a b (Ha,H). destruct (le_exists_sub _ _ H) as (d & EQ & Hd). rewrite EQ. rewrite 2 mul_add_distr_r. rewrite !add_assoc. apply add_le_mono_r. rewrite add_comm. apply add_le_mono_l. apply mul_le_mono_nonneg_l; trivial. order. - intros a b Ha Hb. destruct (le_gt_cases a b). + apply AUX; split; order. + rewrite (add_comm (b*a)), (add_comm (a*a)). apply AUX; split; order. Qed.
imports: NZAxioms NZAddOrder