proposition: Lemma Product_tau_cone_law : Cone_law Product_tau.
proof: Proof. unfold Cone_law, Product_tau in |- *; simpl in |- *. intros a' b g; elim g; simpl in |- *; intro i. unfold FMor in |- *; simpl in |- *. apply Idr. Qed.
imports: Limit Discr Products